# Rigidity of the Turing degrees

> Claims every symmetry of the Turing degrees is trivial, settling the rigidity question. Plain-English explainer, Lean status and sources.

Canonical: https://closedform.nishachay.tech/e/openai-math-2026-241/
Last updated: 2026-10-14

**Claims every symmetry of the Turing degrees is trivial, settling the rigidity question.**

**Trust:** Formal proof listed · **Papers:** 1 · **First paper:** September 24, 2026 · **Field:** Mathematical logic · **Entry:** 241

*Explained by AI.* Drafted by one AI model and checked sentence by sentence against the paper by a different one. Spot a mistake? Report an error.

Turing degrees group sets of whole numbers by how hard they are to compute. They are ordered by which ones can compute which. The rigidity question asked whether this order could be shuffled without changing its shape. The paper says no: every such shuffle leaves each degree where it was. A Lean proof checks this main theorem.

## At a glance

- **First step:** 2005 (Theodore Slaman and W. Hugh Woodin, the fixed cone above 0'' and the arithmetic representation)
- **Significance:** Major. It answers a long-standing central question about the structure of relative computability.
- **Trust:** Formal proof listed
- **Field:** Mathematical logic (1 paper)

## The explanation

Here is the counting trick at the heart of the paper. Pick a hidden number t between 0 and 1, say t = √2 − 1, about 0.41421. Start a running total at 0. At each step, add δt or δ(t − 1), with δ = 1/2. Record a 0 for the first choice and a 1 for the second. A simple rule keeps the total near zero: take the downward step whenever the total is positive. After N steps, the total equals δ(Nt − number of 1s)[1]. If the total stays between −1 and 1, the share of 1s is within 1/(Nδ) of t[2]. With N = 1000 the rule gives 414 ones, so the guess is 0.414. The bound promises an error under 1/500, and the real error is about 0.0002. So a list of yes-or-no choices can recover a number.

Now the setting. Take two sets of whole numbers, A and B. A is Turing reducible to B when a program that may ask questions about B can compute A. Sets that compute each other have the same Turing degree. The degrees, ordered by this relation, form a partial order: some pairs are comparable and some are not. An automorphism is a one-to-one relabelling of all degrees that keeps the order exactly. The identity, which moves nothing, is one such map. The rigidity conjecture asks whether it is the only one.

A lot was known before. Every automorphism keeps the Turing jump, which sends a degree to its own halting problem[3]. Slaman and Woodin showed every automorphism fixes all degrees above 0'', the second jump of the computable degree[4]. Below that cone, the question stayed open. The obstacle is that an automorphism is any map at all. It need not be computable, continuous or even definable.

The paper claims that every automorphism is the identity, with no extra assumptions on it[5]. An outside input from Slaman and Woodin represents each automorphism by a well-behaved Borel function on sets of numbers. A Borel function is one built from continuous pieces by countable limits. The paper uses that function to run the counting trick. Four values of the function, at shifted copies of t, let a program rebuild t[6]. Two extra helper numbers enter, but typical helpers carry no useful information, so they drop out[7]. This shows each degree sits above its own preimage. Running the same argument in both directions forces equality. The paper also states a consequence: Slaman and Woodin's biinterpretability conjecture follows[8].

How sure is this? A computer proof checker called Lean has a formal proof of the main theorem. It covers every order automorphism of the full Turing degrees, with no definability assumption. The paper's extra representation corollaries are not part of that check. No specialist review of the paper has been published.

**What it doesn't show.** This does not cover the paper's extra representation corollaries in the Lean check, or say anything about other degree structures.

## Where it came from

This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026.

## Hype check

The main theorem has a Lean proof. Its weight in computability theory is large. The corollaries outside the Lean statement rest on the paper alone. No specialist review is published.

## Words used

- **Turing reducible:** A is reducible to B when a program allowed to ask questions about B can compute A.
- **Turing degree:** A class of sets of whole numbers that can each compute the others.
- **Automorphism:** A one-to-one relabelling of a structure that keeps all its relations exactly.
- **Turing jump:** The halting problem relative to a given set: which programs that ask about the set eventually stop.
- **Borel function:** A function built from continuous pieces by repeated countable limits; a broad class of well-behaved functions.
- **Comeager:** Large in the sense of category: everything except a countable union of nowhere-dense sets.

## The original paper

- [Rigidity of the Turing degrees](https://github.com/openai/math/blob/main/preprints/Rigidity-of-the-Turing-degrees-September-24-2026/paper.pdf) - September 24, 2026 · Formal proof listed

- [Lean notes](https://github.com/openai/math/blob/main/lean/docs/241.md)

## Quoted lines from the paper (8)

[1] From [Rigidity of the Turing degrees](https://github.com/openai/math/blob/main/preprints/Rigidity-of-the-Turing-degrees-September-24-2026/paper.pdf):

> Summing these increments gives \[ s_N=\delta\left(Nt-\sum_{n<N}r_n\right). \]

[2] From [Rigidity of the Turing degrees](https://github.com/openai/math/blob/main/preprints/Rigidity-of-the-Turing-degrees-September-24-2026/paper.pdf):

> If the states remain in $(-1,1)$, the proportion of choices with $r_n=1$ approximates $t$ with error less than $1/(N\delta)$.

[3] From [Rigidity of the Turing degrees](https://github.com/openai/math/blob/main/preprints/Rigidity-of-the-Turing-degrees-September-24-2026/paper.pdf):

> Using Slaman and Woodin's definability of the double jump, Shore and Slaman proved that the jump is definable from the ordering, so every order automorphism preserves it.

[4] From [Rigidity of the Turing degrees](https://github.com/openai/math/blob/main/preprints/Rigidity-of-the-Turing-degrees-September-24-2026/paper.pdf):

> Slaman and Woodin obtained a fixed cone common to all automorphisms: every automorphism fixes all degrees above $\mathbf0''$, the second jump of the computable degree.

[5] From [Rigidity of the Turing degrees](https://github.com/openai/math/blob/main/preprints/Rigidity-of-the-Turing-degrees-September-24-2026/paper.pdf):

> Every order automorphism of the full Turing-degree structure is the identity: \[ \forall\pi\in\Aut(\DT,\leT)\ \forall\mathbf a\in\DT \qquad \pi(\mathbf a)=\mathbf a. \]

[6] From [Rigidity of the Turing degrees](https://github.com/openai/math/blob/main/preprints/Rigidity-of-the-Turing-degrees-September-24-2026/paper.pdf):

> For a Borel map $F:\R\to2^\N$ with countable fibers satisfying \[ F(x+y)\leT F(x)\oplus F(y), \] we recover any prescribed irrational $t\in(0,1)$ from four values of $F$ at rational affine combinations of $t$ and two auxiliary reals $u,v$.

[7] From [Rigidity of the Turing degrees](https://github.com/openai/math/blob/main/preprints/Rigidity-of-the-Turing-degrees-September-24-2026/paper.pdf):

> Since recovery holds on a comeager set, Lemma … removes the auxiliary degrees and yields $\pi^{-1}(\mathbf a)\leT\mathbf a$ for every degree $\mathbf a$.

[8] From [Rigidity of the Turing degrees](https://github.com/openai/math/blob/main/preprints/Rigidity-of-the-Turing-degrees-September-24-2026/paper.pdf):

> Theorem … also settles the biinterpretability conjecture of Slaman and Woodin.

## Other sources

- [openai/math, Lean scope note for family 241](https://github.com/openai/math/blob/main/lean/docs/241.md): “every order automorphism of the full Turing degrees of subsets of $\mathbb N$ fixes every degree, with no definability or genericity assumption”
- [openai/math release notes (2026): model provenance and review status](https://github.com/openai/math/blob/main/README.md): “manuscripts and supporting proof artifacts produced by an internal OpenAI model”

## Related

- [Shelah's eventual categoricity and the prescribed-threshold obstruction](https://closedform.nishachay.tech/e/openai-math-2026-240/) - Mathematical logic
- [Single-fold Diophantine representations and undecidability under an at-most-one-solution promise](https://closedform.nishachay.tech/e/openai-math-2026-242/) - Mathematical logic
- [Separating choiceless counting from polynomial time and witnessed choice](https://closedform.nishachay.tech/e/openai-math-2026-243/) - Mathematical logic
- [The Partition Principle does not imply Choice](https://closedform.nishachay.tech/e/openai-math-2026-244/) - Mathematical logic
- [Weak normalization implies strong normalization in pure type systems](https://closedform.nishachay.tech/e/openai-math-2026-245/) - Mathematical logic
- [Mathematical logic](https://closedform.nishachay.tech/science/mathematics/mathematical-logic/) - Field · 6 results
- [Open since the 2000s](https://closedform.nishachay.tech/open-since/2000s/) - Era · 48 results
- [Lean-checked results](https://closedform.nishachay.tech/trust/lean-checked/) - Trust · 242 results
- [Report an error](https://github.com/nishachay/closed-form/issues/new?template=report-error.yml&labels=entry-error&title=%5Bentry%20241%5D%20)
