Sakoda–Sipser, settled?

0:00Two-way automata

A finite automaton reads a word one letter at a time, with a fixed number of internal states. A two-way automaton may also move its reading head back to the left, as often as it likes. That adds no power: two-way machines recognize exactly the same languages as one-way ones, as Rabin and Scott, and Shepherdson, showed in 1959. But it can change how many states are needed. Nondeterminism is the other dial: a nondeterministic machine may guess, and it accepts if some guess leads to acceptance. The question is the price, in states, of removing those guesses while keeping two-way motion. In 1978, Sakoda and Sipser asked how many states a two-way deterministic machine needs to simulate a nondeterministic one, and conjectured that the answer is exponential. Their complete problem for one-way nondeterministic machines is now called one-way liveness. Each letter is a binary relation on h points, drawn as arrows between two columns of h dots. A word is live if some path runs through all the columns, left to right. A nondeterministic machine with h + 3 states guesses the path and never moves left. A one-way deterministic machine must track the set of reachable points, which takes 2^h states. Against unrestricted two-way deterministic machines, the lower bounds the liveness paper cites are quadratic; exponential bounds were known only for restricted machines, such as sweeping ones, which turn around only at the ends. In our check, the guessing machine was right on 9,000 random words, and the one-way count is exactly 2^h for h up to 4.

1:45The claim

Result 129 is two OpenAI preprints, of 20 and 18 pages, both dated September 25. The first claims that every two-way deterministic machine for one-way liveness on h points needs roughly 2^(h/62) states, while the nondeterministic machine has only h + 3. The second claims that complementing two-way nondeterministic machines is also exponential: for a machine with n states recognizing liveness, every two-way nondeterministic machine for the complement needs roughly 2^(n/127) states. Since two-way deterministic machines can be complemented cheaply, this gives a second, weaker deterministic bound for the same family. The alphabets grow: liveness on h points uses all 2^(h²) relations as letters. That is allowed in Sakoda and Sipser’s question, where the polynomial may not depend on the alphabet, and the release says this resolves their conjecture in that form. Nothing is claimed for a fixed alphabet, such as two letters, and the papers say they give no separation of logarithmic-space complexity classes. The rates are slow: the deterministic bound first exceeds the size of the nondeterministic machine at h equals 653, but at h equals 2,002 it is over 2 billion states. OpenAI published a Lean formalization of all three bounds, 41 files and about 8,500 lines with imports, not counting Mathlib. We have not run the Lean check.

3:22How the proofs go

The deterministic bound starts from configurations, a state and a head position. Add a sink after acceptance. Because each configuration has at most one successor, the configurations that eventually reach the sink form a tree. Walk around that tree, along both sides of every edge. Cut the tape into cells: each cell’s share of this doubled wiring, built for every state at once, becomes a perfect matching between ports on its two sides, 4(s + 1)² ports per side, and it depends only on that cell’s letter, because every possible transition gets a reserved slot. Glue the matchings of a word, and the machine accepts exactly when a test port on the left is joined to one on the right. In our check, we built these matchings for 240 random small machines, and they decided acceptance correctly on all 6,000 words. Two words with the same glued matching behave the same in every context. Liveness tells apart any two different relation products: put a single-point letter on each side, and only one of the surrounded words stays live. So the matchings generated by the letters map onto the monoid of all binary relations on h points, preserving multiplication. The proof shows that this needs exponentially many ports. The rank of a matching counts the strands that cross from left to right, and multiplying never increases it. An idempotent, a matching equal to its own square, has a corner that behaves like a smaller matching monoid on its crossing strands alone. Take an idempotent matching that maps to the identity relation plus one extra pair. The claim is that it must lose at least L(h) crossing strands, where L(h) is 2^⌊(h − 2)/31⌋. The induction uses 32 conjugates of that idempotent to build 256 successive additions of a pair, all sharing one support budget. Each addition contains a corner representing all relations on 31 fewer points, so by induction it loses at least ½ L(h − 31). The shared budget is 64 times the original loss, and 256 of these half-losses must fit inside it, so the bound doubles every 31 points. Since the number of ports is at least the lost rank, 4(s + 1)² is at least 2^⌊(h − 2)/31⌋; if acceptance must come after at least one move, s + 1 becomes s + 2. For the complement, the machine stays nondeterministic, so its computations no longer form a tree. Instead, each letter becomes a path diagram: four relations recording how a computation can enter and leave a cell, passing through in either direction or turning back. These diagrams multiply by joining boundaries, forming the monoid of partitioned binary relations of Martin and Mazorchuk. Adding edges only adds accepting paths, but the complement accepts when the product is empty, so the map to relations reverses inclusion. The proof tracks classes of labels that a repeated diagram keeps returning to, and how many of them each added pair destroys, which a fixed context can at most double; with a larger amplification, the bound doubles every 127 points. In our check, the path diagrams of 300 random small nondeterministic machines decided acceptance correctly on 7,500 words.

6:57Where it stands

The preprints are not peer reviewed and have not been revised. The Lean formalization covers the complementation bound, the deterministic bound for the same family, and the liveness bound; we have not run it. Neither paper is among those OSVerify reviewed, and we have seen no expert review. If they hold, two-way nondeterministic automata can be neither complemented nor determinized with polynomially many states, uniformly over alphabets, answering Sakoda and Sipser’s question in its standard form after nearly fifty years. The versions over a fixed alphabet, and the question of L versus NL, are not touched.