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. (Lean)
Manuscript
Rigidity of the Turing degrees
September 24, 2026 · source · Lean formalization available · cite as \cite{OAI:Rigidity-of-the-Turing-degrees-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.
Result 241 · Mathematical logic. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.
Source: https://github.com/openai/math/blob/main/CONTENTS.md