Rigidity of the Turing degrees

Follow-up works

• B. Kjos-Hanssen, Baire measurable functions and automorphisms of the truth-table degrees (arXiv:2610.16059, October 2026). Adapts this paper's proof to truth-table (and weak truth-table) reducibility for automorphisms induced by Baire measurable functions, noting that the Turing-degree decoding is an unbounded search and so not a truth-table reduction. Its acknowledgments state assistance from Claude and a Lean 4 formalization with Aristotle (Harmonic), in bjoernkjoshanssen/tt-auto.

Comments and discussion

• Commenter "Patrick" and others on Computational Complexity, comment thread of Conjectures that I thought would not be proved in my lifetime....were (blog comments, 11–13 Oct 2026). Patrick writes that the rigidity proof "is a short proof and not hard to follow" and links Andrew Marks's exposition; later commenters ask whether humans in the area could have found it.

Formalization

• OpenAI math release, Lean scope note lean/docs/241.md (release Lean docs, October 2026). States that Lean formalizes the main theorem, that every order automorphism of the Turing degrees of subsets of ℕ fixes every degree, with no definability or genericity assumption; the representation corollaries are not formalized. [AI-generated per source]
• OpenAI, comparator statement ComparatorChallenges/DegreeRigidity.lean (openai/math, October 2026). Defines Turing degrees as the antisymmetrization of Mathlib's TuringReducible on ℕ → Bool and states MainTheorem : ∀ π : Degree ≃o Degree, ∀ a, π a = a.
• OpenAI, Lean proof OAI/Computability/DegreeRigidity/Main.lean (openai/math, October 2026). Proves rigidity from a borel_representation lemma, itself obtained from an imported global_arithmetic_generic_program lemma rather than taken as a hypothesis; the directory includes CohenForcing, Constructibility, SetModels and Representation subfolders.

Related prior literature mentioned by others

• Theodore A. Slaman and W. Hugh Woodin, Definability in Degree Structures (unpublished manuscript, July 21, 2005). Marks's exposition invokes Theorem 6.3.1(2), the arithmetic representation of every degree automorphism, as the input to the rigidity argument.
• A. S. Kechris, Classical Descriptive Set Theory (Springer, 1995), Theorem 9.10, as cited by A. Marks (book, 1995). Marks says the key lemma is reminiscent of the proof that Baire measurable homomorphisms of Polish groups are continuous; this reference is not in the paper's bibliography.
• M. J. Groszek–T. A. Slaman (1998) and P. Lutz–B. Siskind, Part 1 of Martin's Conjecture for order-preserving and measure-preserving functions, as cited by A. Marks (BSL 1998; arXiv:2305.19646, JAMS 38, 2025). Marks calls their coding tricks "somewhat reminiscent" of the argument; the paper itself already cites both as related finite-oracle recovery results.

Possibly relevant literature (found by the agent, not checked)

• T. A. Slaman and M. I. Soskova, The Δ⁰₂ Turing degrees: Automorphisms and Definability (preprint, submitted to the London Mathematical Society). Local analogue of the global Slaman–Woodin results the paper builds on: rigidity of D_T(≤0′) is equivalent to its biinterpretability with first-order arithmetic; compare the paper's biinterpretability corollary.
• R. A. Shore, Rigidity and biinterpretability in the hyperdegrees (preprint dated 31 Oct 2005). Proves rigidity and biinterpretability with second-order arithmetic for the hyperarithmetic degrees by coding arguments, a precedent for the paper's conclusions in a coarser degree structure.

Digests and expositions

• A. Marks, Rigidity of the Turing degrees (after OpenAI) (expository note, 3 pp., 7 Oct 2026). Re-proves the key lemma X ≤_T F(X) ⊕ F(G) ⊕ F(H) for arithmetically X-generic pairs (G,H) using arithmetic Cohen forcing and 2-adic addition on Cantor space, with the Slaman–Woodin representation as the only external input; it describes the result as completing Slaman and Woodin's argument and acknowledges ChatGPT-Astra proofreading.
• Open Mathematics Courses, The rigidity of the Turing degrees (course, undated). Four lessons written and self-checked by Claude Opus 5.5 explain relative computability, category avoidance, four-value recovery and rigidity, taking the Slaman–Woodin representation theorem as a named hypothesis and stating that independent review is incomplete. [AI-generated per source]

News and blogs

• W. Gasarch, Conjectures that I thought would not be proved in my lifetime....were (Computational Complexity blog, 11 Oct 2026). Item 6 discusses this result, giving Rogers's 1960s question, the Slaman–Woodin background and the Lean formalization, and says "very few people" work on the problem, so understanding the proof may take a while.
• Azmat, Rigidity of the Turing Degrees: How OpenAI’s Proof Eliminates Every Hidden Symmetry (Binary Verse AI, October 18, 2026). Explains the paper's Borel representation, four-oracle recovery and category-avoidance steps, and distinguishes its account of the reported Lean scope from an independent formalization audit.