Lean formalization in OpenAI math repository (Result 137)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Simulating One-Tape Time in Two-Fifths-Power Space'. We show that a fixed deterministic Turing machine with one writable tape and head can be simulated in O(T^{2/5}\mathop{\mathrm{polylog}}\nolimits (T+2)) work-space bits when a binary time cap T ≥ 2 is supplied. The simulator computes the finite-control and halting outcome by time T; its running time is unrestricted. The result allows a fixed number of read-only input heads and requires a fixed accessor that supplies every initial writable and read-only symbol within distance T of the relevant head origin in polylogarithmic space. This improves the square-root space exponent for one-tape machines, answering Williams's question for this model.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 137). The Lean development was not rebuilt locally.