Lean formalization in OpenAI math repository (Result 129)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'An exponential two-way deterministic state lower bound for one-way liveness'. One-way liveness on h points accepts a word of binary relations when their ordered product is nonempty. For every h ≥ 2, it has a nondeterministic automaton with h+3 states and no left moves, whereas every equivalent s-state two-way deterministic automaton satisfies 4(s+2)^2\ge2^{\lfloor(h-2)/31\rfloor}. Partial transition rules, stay moves, and nonaccepting infinite computations are allowed. The alphabets are finite and grow with h, so the result rules out an alphabet-independent polynomial state bound for deterministic two-way simulation, already for one-way nondeterministic sources.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 129). The Lean development was not rebuilt locally.