Theoretical computer science · Result 137

One-tape time simulation in two-fifths-power space

1 paperLean

Determines the halting and finite-control outcome of a fixed deterministic one-writable-tape machine up to time T using \(O(T^{2/5}\log^C(T+2))\) space, improving the square-root exponent. Heads move at most one cell per step; finitely many read-only input heads are allowed. Initial contents are independent of T, and contents and input symbols have polylogarithmic-space access. Simulation time is unrestricted.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

Simulating One-Tape Time in Two-Fifths-Power Space

OpenAI · September 25, 2026

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.

Read PDF Download Source

Cite

@misc{OAI:Simulating-One-Tape-Time-in-Two-Fifths-Power-Space-September-25-2026,
  author = {{OpenAI}},
  title = {{Simulating One-Tape Time in Two-Fifths-Power Space}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Simulating-One-Tape-Time-in-Two-Fifths-Power-Space-September-25-2026/article.pdf}{OAI:Simulating-One-Tape-Time-in-Two-Fifths-Power-Space-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Simulating One-Tape Time in Two-Fifths-Power Space

Scope

The formalization gives two-fifths-power space simulation of a fixed deterministic machine with one writable tape and finitely many read-only input heads. Heads move at most one cell per step, initial contents are independent of the time bound, and contents and input symbols must be accessible in polylogarithmic space. Given a binary time cap \(T\ge2\), the simulator returns the source's finite-control outcome and halting flag using \(O(T^{2/5}(\log(T+2))^C)\) space.

A second simulator needs no time cap: on an input that halts at time \(t\), it returns the halted outcome using \(O((t+2)^{2/5}(\log(t+2))^C)\) space. Simulation time is unrestricted. General multitape simulation, hierarchy consequences, and bounded-space-halting results are outside these selected statements.

Comparator links

Result	Comparator statement
Time-capped and unknown-time one-tape simulation in two-fifths-power space	OneTapeSpace.lean

Scope note on GitHub →