Rigidity of the Turing degrees
Rigidity of the Turing degrees is the subject of a manuscript dated 24 September 2026 in OpenAI's public mathematics collection (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 Rigidity of the Turing degrees, dated 24 September 2026.
- Formalization, as described by the repository. The scope note 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
| Date | Work | Relation | Public claim | Public status (checked 14 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math at commit adc7f12, tables at repository commit cd0063d, 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 DegreeRigidity (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, 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ω to 2ω, 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.