Rigidity of the Turing degrees: is every automorphism of the Turing degrees the identity?
The Turing degrees are the classes of subsets of under mutual Turing reducibility, partially ordered by . Jockusch and Solovay showed jump-preserving automorphisms fix every degree above ; Shore and Slaman showed the jump is definable, so every automorphism preserves it; Nerode and Shore showed each automorphism fixes a cone; and Slaman and Woodin showed every automorphism fixes all degrees above , that the automorphism group is countable, and that rigidity is equivalent to their biinterpretability conjecture. The rigidity problem asks: is every order automorphism of the identity?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Computability theory; degrees of unsolvability
- Posed by
- Classical problem of degree theory; equivalent (Slaman-Woodin) to the Slaman-Woodin biinterpretability conjecture
- Year posed
- —
- Years open
- —
- Solved
- 2026-09-24
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 50 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: every order automorphism of is the identity. The proof represents an arbitrary automorphism by an arithmetic, hence Borel, map on reals (Slaman-Woodin), recovers any irrational from four values of such a map at rational affine combinations of it and two auxiliary reals, for a comeager set of auxiliary pairs, and removes the auxiliaries by Sacks-type category cone avoidance. As a corollary it settles the Slaman-Woodin biinterpretability conjecture positively. It does not address rigidity of other degree structures such as the computably enumerable degrees or the degrees below .
What the AI did
The release README says every result in openai/math was produced by an unreleased internal OpenAI model with a fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result. This result is not one of the README's two exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region). The manuscript is authored 'OpenAI' and names no human author. The manuscript is short (five sections). Its external input is the Slaman-Woodin representation theorem from their 2005 unpublished manuscript; the proof adds a four-value recovery argument for Borel maps and a category cone-avoidance step.
Verification
No independent mathematician has checked this yet. Checked here: Theorem 1.1 was read against the rigidity problem; it states that every order automorphism of the full Turing degrees is the identity, in ZFC, with no definability hypothesis on the automorphism. Lean: lean/formalization.yaml lists comparator DegreeRigidity with declaration OAI.TuringRigidity.ManuscriptMain.rigidity. The statement ComparatorChallenges/DegreeRigidity.lean was read here: it defines oracles as Bool, reduction by Mathlib's TuringReducible on their characteristic functions, Degree as the antisymmetrization, and asserts that every order isomorphism Degree to Degree fixes every degree. This is the headline claim. The Lean development (OAI/Computability/DegreeRigidity, with forcing, constructibility and set-model subdirectories) derives the Borel representation inside Lean rather than assuming the Slaman-Woodin input. Not rebuilt here. Permitted axioms: propext, Quot.sound, Classical.choice.