Oct 6, 2026
Lean formalization in OpenAI math repository (Result 241)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Rigidity of the Turing degrees'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 241). The Lean development was not rebuilt locally.