One-tape time simulation in two-fifths-power space
From OpenAI Aftermath
One-tape time simulation in two-fifths-power space concerns how much memory suffices to reproduce T steps of a Turing machine with a single writable tape when the simulation may take arbitrarily long. A space bound of about √T is classical for this model, and in 2025 Williams showed that multitape time t can be simulated in space about √(t log t); Williams asked whether the one-tape exponent 1/2 can be lowered by a fixed positive constant. A manuscript dated 25 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims the exponent 2/5 for this model, with a Lean formalization. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- In Williams's account, the classical square-root space bound for one-tape machines goes back to Hopcroft and Ullman. Williams proved that deterministic multitape time t(n) can be simulated in space O(√(t(n) log t(n))), building on the tree-evaluation algorithm of Cook and Mertz; the interpolation viewpoint behind that algorithm is also explained by Goldreich.
- In Section 5 of the full version of his paper, Williams asks whether the classical one-tape bound can be improved by a fixed positive constant in the exponent.
The original result
- Claim. The main theorem of Simulating One-Tape Time in Two-Fifths-Power Space states that for a fixed deterministic machine with one writable tape and finitely many read-only input heads, every head moving at most one cell per step, and initial contents independent of the time cap and accessible in polylogarithmic space, the finite-control outcome and halting status at time T can be computed from a binary time cap T ≥ 2 in O(T2/5 logC(T + 2)) bits of work space; the running time of the simulator is unrestricted. A second form needs no time cap: on an input that halts at time t it returns the outcome in O((t + 2)2/5 logC(t + 2)) space. The manuscript states that this answers Williams's question for this model, and it gives no log-free bound at exponent 2/5.
- Method, as described: the writable tape is divided into shifted blocks, so that one offset has few block visits; a visit exchanges only a short controller, and all visits to a block can be replayed from its initial contents once a controller transcript is fixed. Visits are grouped into epochs whose controllers are appended in rounds, with at most one retained round guess per epoch on a recursion path, and the factored word recurrences are evaluated in the style of Cook and Mertz with one fixed pool of registers, which gives the exponent 2/5.
- Source (openai/math repository, commit
7ef5c0c): Simulating One-Tape Time in Two-Fifths-Power Space, dated 25 September 2026. - Formalization, as described by the repository. The scope note lean/docs/137.md states that the formalization gives the time-capped and the unknown-time simulators in two-fifths-power space, and that general multitape simulation, hierarchy consequences and bounded-space halting results are outside the selected statements. The Comparator statement is
OneTapeSpace.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 30 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | One-tape computation in two-fifths-power space, an article of the Latent Seminar blog at lowrank.github.io | Reading (exposition) | Explains computation time and workspace, the condition on access to public symbols, shifted blocks and local replay, epochs and rounds with the retained-data invariant, evaluation with a reusable register pool, the derivation of the exponent, and the unknown-time form, with proof outlines. | Blog article; it states that its review covers statements, introductions and selected proof mechanisms and is not an independent verification of the complete proofs. |
| 2026-10-10 | MathVet (GitHub; review of openai/math, tables at repository commit 94c6630, 28 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full": the two Lean clauses are the time-capped and unknown-time parts of the manuscript's main theorem, and the summary's comparison with the square-root exponent is not a separate formal claim. It records a sandboxed Comparator pass for OneTapeSpace on 10 October 2026. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K, run 38019899278 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the OneTapeSpace solution, in 238 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list OneTapeSpace, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-13 | One-tape time in two-fifths-power space, a course on Open Mathematics Courses (kokunoyumeto/open-math-courses-public) | Reading (exposition) | Five lessons with a complete proof: one-tape machines, blocks and visits; polynomials for Boolean functions; an evaluator with one pool of registers; histories, checkpoints and the theorem; and several writable tapes with lower bounds for time, where the space hierarchy theorem is a named hypothesis. | The course states that it was written and self-checked by Claude Opus 5.5 (Anthropic) and that independent review is not complete. |
| 2026-10-16 | AI Proved What?, episode 137 Below the square root?, remade version of 26 October 2026 | Reading (exposition) | Video explainer of the claim and its relation to Williams's multitape theorem. The episode states that no useful bound on the simulator's running time is claimed, so the result cannot be iterated as a speedup; that for several writable tapes the manuscript proves only the square-root scale again; that optimality and a log-free bound are not claimed; and that by the site's arithmetic the gain T1/10 exceeds one factor of log2 T only beyond about 259 steps. | Web page and video; the site states that its scripts and animations are produced with AI assistance and that the narration is an AI-generated voice. Status record last checked 27 October 2026: posted as a preprint: OpenAI, 17 pages, dated September 25, 2026; under expert review: not yet; peer reviewed: not yet; checked in Lean: the main theorem with and without a time cap, added on October 7, 2026, not run by the site. The page states that the hierarchy corollaries and the multitape comparison are not formalized and that it has seen no expert review. |
Notes
- The background summarizes the manuscript's own account of earlier work.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
