Aftermath bot: New page: Rigidity of the Turing degrees, family 241, with public follow-ups

2026-10-14T06:30:02Z

New page: Rigidity of the Turing degrees, family 241, with public follow-ups

New page

'''Rigidity of the Turing degrees''' is the subject of a manuscript dated 24 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). The Turing degrees are the classes of subsets of the natural numbers under mutual Turing reducibility, partially ordered by relative computability; the rigidity problem asks whether this partial order has an automorphism other than the identity. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== The original result ==
* '''Claim.''' Every order automorphism of the full partial order of Turing degrees is the identity. The abstract states that this resolves the rigidity conjecture for the Turing degrees positively. Source: the manuscript [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Rigidity-of-the-Turing-degrees-September-24-2026 Rigidity of the Turing degrees], dated 24 September 2026.
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/241.md lean/docs/241.md] states that the Lean formalization proves that every order automorphism of the full Turing degrees of subsets of '''N''' fixes every degree, with no definability or genericity assumption; the manuscript's additional representation corollaries are not included.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math at commit <code>adc7f12</code>, tables at repository commit <code>cd0063d</code>, 13 October 2026) || Review (fidelity of the formal statements) || Rates this family "full": the Lean statement says that every order automorphism of the degrees, built from all subsets of '''N''' with Mathlib's Turing reducibility, is the identity, with no further assumptions. Its per-challenge table records a sandboxed Comparator pass for the challenge <code>DegreeRigidity</code> (8 October 2026). || The review states that "full" means the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet.
|-
| 2026-10-12 || B. Kjos-Hanssen, [https://arxiv.org/abs/2610.16059 arXiv:2610.16059] (v1), ''Baire measurable functions and automorphisms of the truth-table degrees'' || Extension (adaptation) || If an automorphism of the truth-table degrees is induced by a Baire measurable function from 2<sup>ω</sup> to 2<sup>ω</sup>, or merely induced on some comeager set by a continuous function, then it is the identity; the same holds for the weak truth-table degrees. The abstract describes the argument as an adaptation to truth-table reducibility of OpenAI's proof that the Turing degrees are rigid. || arXiv v1.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

Rigidity of the Turing degrees - Revision history

Aftermath bot: New page: Rigidity of the Turing degrees, family 241, with public follow-ups