Oct 6, 2026
Lean formalization in OpenAI math repository (Result 129)
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 'An exponential state lower bound for two-way nondeterministic complementation'. We prove that two-way nondeterministic finite automata cannot be complemented with a polynomial number of states independent of the alphabet. For each n ≥ 4 we construct an n-state automaton over a finite alphabet whose complement requires at least \tfrac12 2^{\lfloor(n-4)/127\rfloor}-1 states.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 129). The Lean development was not rebuilt locally.