Below the square root?

0:00Time versus space

How much memory do you need to reproduce a computation, if you may take as long as you like? Take a Turing machine with a single tape it can write on, and a head that moves at most one cell per step. Here is one we built that checks whether 0110110 is a palindrome: it erases the first symbol, runs to the far end, compares, erases, and walks back. It accepts after 36 steps. Draw time going down and the tape across, and the head zigzags. Now count how often it crosses each boundary between cells: 3, 5, 7, 8, 6, 4, 2. The middle boundaries carry the traffic, and the counts add up to 35, one for each step that moves. So a running time T is also a budget of at most T crossings. Simulating a one-tape machine that runs for T steps in about √T space is classical; the paper, following Ryan Williams’s account, attributes it to Hopcroft and Ullman. In 2025, Williams showed that a multitape machine running for time t can be simulated in space about √(t log t), building on the tree evaluation algorithm of Cook and Mertz. That did not lower the one-tape exponent of one half, and Williams asked whether, for one-tape machines, it could be lowered by a fixed positive constant.

1:21The claim

Result 137 is a single OpenAI preprint, 17 pages, dated September 25. It claims the answer is yes, for this model: one writable tape, any fixed number of read-only input heads, every head moving at most one cell per step, and fixed starting contents, independent of the cap, that a small accessor can look up in polylogarithmic space. Given such a machine, its input and a time cap T, the machine’s state, and whether it has halted by time T, can be computed deterministically with about T^(2/5) bits of memory, times logarithmic factors, not counting the input. If the machine halts but its running time is not supplied, the same holds with the actual running time t in place of T. Two fifths is one half minus one tenth, so the bound beats the square root by a fixed power. The paper is careful about limits. The simulation can be astronomically slow: it gives no useful bound on its own running time, so it cannot be iterated as a speedup. It does not cover machines with several writable tapes; for those, the paper proves only a square-root bound again. It claims no optimality, and the gain is asymptotic: T^(1/10) is about four at a million steps and sixteen at a trillion, and by our arithmetic it outgrows even a single factor of log₂T only beyond about 2^59 steps. The main theorem, in both versions, is formalized in Lean: 49 files, about 8,300 lines, with no sorry. The paper’s hierarchy corollaries are not.

2:57How the proof goes

The proof first cuts the tape into blocks of width b. A visit lasts until the head leaves its block. Each move crosses a block boundary for exactly one of the b ways to shift the grid, so some shift sees at most T/b crossings, and so at most one more visit than that. The simulator simply tries every shift. Between visits, all that passes from one block to the next is a short controller: the state, head positions, the time and a few flags, a few times log T bits. Now guess the whole list of controllers. Each block can check it alone: replay that block’s visits from its starting contents, and compare each result with the next guessed controller. In our run with blocks of width three, the true list passes every block, and changing one state makes the block that hands that controller on, and the block that receives it, both fail. Consistency factors over blocks. Next, group the visits into epochs of b visits, each split into k rounds of k visits, with k about T^(1/5) and b equal to k². Two kinds of words, each about b log T bits, describe the run: the contents of each block at the start of an epoch, and the controllers seen so far within that epoch. One round’s update is a sum over all guesses for the next k controllers, of that guess appended to the history, times one replay check per block, and exactly one guess passes them all. The paper evaluates such sums with its own evaluator, built on the shared-memory idea of Cook and Mertz, in the interpolation form Goldreich described: words become vectors over a finite field, each rule becomes a low-degree polynomial, and the key procedure adds a multiple of a value into one register and restores every other register, whatever they held before. So nested calls borrow one shared pool of memory instead of each needing its own. The memory then has two parts: the width of a word, about b up to log factors, and a stack along the longest chain of dependencies. Within an epoch, a chain takes at most k cheap steps, then pays at most once, about k log T bits, to hold a guess while it recomputes a block from the epoch before. With about T/b² epochs, the stack is about T/b², times √b. Balancing the two gives b about T^(2/5). In our table, ignoring log factors, at a billion steps the two parts are about 4,000 each, against about 32,000 for the square root. The paper also explains why tuning this construction’s scales cannot beat two fifths, and why it needs a single writable tape: with two tapes, a step can depend on whether two bits are equal, and that test is not a product of checks on each bit.

5:41Where it stands

The preprint is not peer reviewed and has not been revised. The Lean proof of the main theorem was added to the repository on October 7; we did not build it or run the comparator. The hierarchy corollaries and the multitape comparison are not formalized. The paper is not among those OSVerify reviewed, and we have seen no expert review. If it holds, Williams’s one-tape question has a positive answer for this model: one-tape time T fits in about T^(2/5) space, below the classical square root by a fixed power. The paper claims no such improvement for machines with several writable tapes, and no bound at all on how long the simulation takes.