∑math20

Mathematical logic · Result 241

Rigidity of the Turing degrees

1 paperLean

Every order automorphism of the Turing degrees is the identity, resolving their rigidity problem. Thus no nontrivial relabeling of degrees preserves the ordering by relative computability.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Rigidity of the Turing degrees

Rigidity of the Turing degrees

OpenAI · September 24, 2026

We prove that every order automorphism of the full partial order of Turing degrees is the identity, resolving the rigidity conjecture for the Turing degrees positively.

Read PDF Download Source

Cite
@misc{OAI:Rigidity-of-the-Turing-degrees-September-24-2026,
  author = {{OpenAI}},
  title = {{Rigidity of the Turing degrees}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Rigidity-of-the-Turing-degrees-September-24-2026/paper.pdf}{OAI:Rigidity-of-the-Turing-degrees-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The rigidity problem asks whether the ordering of Turing degrees by relative computability has any nontrivial automorphism. The formalized result gives a negative answer: every order automorphism of the full Turing degrees of subsets of \(\mathbb N\) fixes every degree, with no definability or genericity assumption. The additional representation corollaries are not included.

Comparator links

ResultComparator statement
Rigidity of the Turing degreesDegreeRigidity.lean

Scope note on GitHub →