Source and verification

This article explains family 137 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.

🏷️ Preliminaries: computation time and workspace

A deterministic Turing machine’s running time counts transitions. Its workspace counts the writable memory simultaneously in use. Recomputing a value can save space even if it greatly increases time. Family 137 asks how much memory is necessary to recover the outcome of a computation that originally runs for at most steps.

The relevant machine has one writable tape, a finite alphabet, and one head moving by at most one cell per transition. It may also have a fixed number of read-only heads with unit-speed motion. The simulator receives an ordinary endmarked read-only input and a binary cap . Its requested output is the finite-control state and halt/timeout outcome at that cap. It is not required to retain the entire final tape.

The space measurement is in work bits, excluding the simulator’s read-only input. Write for times a fixed power of . Graduate familiarity with algorithms, recursion, and asymptotic estimates is sufficient for the main accounting argument below.

🏷️ The public-symbol access condition

Read-only data need an explicit access model. The manuscript fixes cap-independent initial-symbol functions: the same input and tape coordinate mean the same initial symbol in every simulation. A fixed accessor must recover these symbols at every coordinate using polylogarithmic workspace.

The condition includes coordinates reached by speculative local replays, not only those visited by the actual computation. Otherwise a simulation could hide a difficult computation inside a supposedly free tape lookup. Ordinary input access by rescanning satisfies the condition. If several heads read the same tape, their symbol functions must describe consistent underlying contents.

Manuscript result

For each fixed machine and fixed accessor satisfying this condition at , its capped outcome can be computed deterministically in work bits. If the machine halts after steps and the access condition holds at every cap, the uncapped outcome can be computed in work bits. (OpenAI, 2026)

The theorem supplies no useful bound on the simulator’s running time. The fixed-machine constants and the logarithmic losses are part of the statement. In particular, it implies space for each fixed , not a logarithm-free bound.

The one-writable-tape restriction is substantive. Additional read-only heads fit the model; additional independently writable tapes do not inherit this exponent from the theorem.

🏷️ Shifted blocks and local replay

Partition the tape into blocks of width , allowing different shifts of the block boundaries. Any one head move crosses a boundary for at most one shift. Averaging over shifts therefore gives a partition with visits to blocks.

A visit carries two kinds of information. The block itself contains tape symbols. Its controller consists of the finite state, head positions, clock, and relevant flags, using bits because the machine is fixed.

For a proposed controller transcript, one can check a particular block’s behavior by replaying visits to it from the appropriate initial block contents. This uses one block and the proposed controller data. It does not require a simultaneous materialization of all tape blocks.

The difficulty is obtaining a consistent transcript without saving the entire history. Guessing here is part of a deterministic enumeration: candidates are tested and combined by an exact evaluation procedure. It is not nondeterministic acceptance, and a candidate’s existence is not treated as a free oracle.

🏷️ Epochs, rounds, and the retained-data invariant

Choose up to harmless rounding. Group block visits into an epoch, and group visits into a round. Thus an epoch has rounds. The number of epochs has order

An epoch’s block data or full controller history fits in bits. A round guess occupies only bits. But a recursive algorithm could still fail by retaining too many guesses or too many full words on its stack.

The manuscript organizes dependencies into words representing epoch-start blocks and partial epoch histories. A history depends on the preceding history in the same epoch and on selected epoch-start blocks. A start-block word, in turn, refers only to the previous epoch.

Retained-guess invariant

Along any active dependency path, at most one costly round guess is retained for each epoch. A call that retains such a guess enters an epoch-start block, whose next dependencies belong to an earlier epoch.

Traversing an ordinary preceding-history edge costs only a small suspended frame. Traversing the history-to-block edge costs the retained round guess. There are at most ordinary history edges and one costly edge per epoch. Up to logarithmic factors, the total active path weight is therefore .

The crucial detail is that a round guess is not retained across the recursive call for the preceding history. It is retained across the block call that drops the epoch index. Retaining it across both kinds of calls would invalidate this accounting.

🏷️ Evaluation with a reusable register pool

The dependency graph can have enormous recomputation cost. Its identifiers and local navigation nevertheless require only logarithmic storage; the graph is not stored explicitly.

The evaluation lemma associates a maximum active path weight to a word of width . It bounds space by

Its strength is a reusable-register contract. A call adds a specified multiple of a word’s encoded value to a selected register and restores all other registers. This must work from arbitrary initial register contents. A procedure requiring every temporary register to start at zero could not safely borrow a caller’s partially filled register.

The construction implements the contract using polynomial interpolation over a finite field. At a high level, it adds a child value to a register, evaluates a local expression, and subtracts the child value again. Interpolation isolates the required coefficient while canceling the unknown baseline contents. Recursive calls therefore share a constant-size pool instead of allocating a new full vector at every depth.

This paragraph uses the interpolation lemma as a computational interface; no background development of abstract algebra is needed. What matters for the space claim is that field elements, interpolation counters, local lookups, suspended scalars, and navigation data are all counted. The local lookup procedures themselves make no recursive word-evaluation calls.

For the tape simulation the ordinary dependencies have fan-in at most two, and three vector registers suffice. The word-width contribution includes reusable local scratch; the path-weight contribution includes retained guesses. Sequential forward and reverse calls reuse the same space.

🏷️ Deriving the exponent

The resulting estimate is

The first term stores a block or an epoch history. The last term pays for active round guesses across epochs. Balance the two dominant contributions:

Then and the remaining term is smaller. Trying the finitely many shifted partitions sequentially reuses the same storage; at least one partition has the required visit bound.

One can also let block width , epoch length , and round length vary separately. Ignoring logarithms, the two stack contributions are

Their minimum occurs at . If , the minimized expression is at least a constant times , leading again to the exponent when balanced against storage .

This calculation diagnoses the stated accounting scheme. It is not a lower bound for all possible simulation methods, nor does it prove the exponent optimal.

🏷️ Unknown running time and scope

For a computation that eventually halts, try caps , discard workspace after every timeout, and return only on a genuine halt. The first sufficient cap is at most , so its space bound controls the entire sequence. This argument needs the access condition at every cap and the same initial-symbol functions throughout.

A designated bit of a sequential write-only output can also be monitored by adding its index, a counter, and the monitored bit to the controller. That costs logarithmic extra storage. It does not require storing the whole output stream.

The result illustrates a general proof obligation in space-efficient recursion: identify what is simultaneously alive, not merely the size of one subproblem. Here the saved information has a weighted dependency-path bound, and the register implementation realizes that bound without hidden copies.

Logspace derandomization studies another setting where the memory model is central. Subset Sum time and space gives a complementary example in which regeneration must preserve a specified time budget as well as a memory bound.

🏷️ Key steps and proof outlines

Homogenization makes unknown register contents removable

The reusable-register lemma rests on an exact coefficient identity. Encode a Boolean word by . For a vector over the finite field used by the evaluator, define

At an encoded Boolean word , this is one if and zero otherwise. Therefore a total Boolean lookup has an extension agreeing with on Boolean encodings and homogeneous of degree . Multiple word inputs use a separate copy of this basis for each input.

Homogeneity is essential. The constant-one lookup extends to , not to the literal constant one. Shifting a borrowed register may make its last coordinate zero, so arguments valid only in the affine slice would not support arbitrary register contents. The paper’s “Evaluation along weighted paths” section keeps the homogeneous extension even for predicates that happen to be constant on some semantic inputs. (OpenAI, 2026)

Top coefficients erase the borrowed baseline

Choose distinct field elements and weights

Lagrange interpolation gives for every polynomial of degree at most . If is homogeneous of degree , substitution gives the stronger operational identity

for arbitrary baseline . Each degree- monomial contributes its value at to the top coefficient; all terms involving have lower degree and disappear. The field has more than elements, so the denominators are nonzero. No division by a factorial is used, which matters because the construction works in characteristic two.

A recursive call can consequently add to a borrowed register containing , evaluate a local polynomial there, and subtract . Summing with these weights recovers a function of the semantic value while restoring . The method may enumerate exponentially many Boolean assignments to evaluate a lookup, but it stores only the current assignment, field scalars, and counters. The theorem permits this large running time.

The loop order determines the path weights

At a history vertex, let be the preceding history, the required block words, and a round guess. The semantic identity sums the guessed output times all consistency predicates . Homogeneous extension gives degree in the history argument and degree in each block argument.

The evaluator first shifts the history register, before entering the coordinate or guess loops. Inside those loops it interpolates one block argument at a time, multiplies the resulting scalar into an accumulator, and discards that factor. After all coordinates and guesses are finished, it unshifts the history. Thus a recursive history call suspends only small scalar bookkeeping; a block call suspends the -bit guess. This realizes edge weights one and , respectively, rather than charging on both kinds of edge.

For tape simulation, a costly block call decreases the epoch index. There is therefore at most one retained round guess per epoch along an active path. The ordinary history edges within an epoch cost at most the number of rounds. With and epochs, the path weight is up to logarithmic factors. A constant pool of vector registers contributes the separate term, yielding .

The recursive contract quantifies over every initial assignment to the entire register pool. A child may borrow the caller’s partially accumulated output, but must restore it before returning. This stronger statement is exactly what permits three registers to serve an arbitrarily deep computation. The exponent follows only after this implementation and retained-data analysis justify the space expression being balanced.

🏷️ Manuscripts and verification scope

No family scope page was present at lean/docs/137.md in the pinned snapshot. This does not establish that all related formalization code is absent. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.

OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.

🐻  OpenAI 2026. Simulating One-Tape Time in Two-Fifths-Power Space.