VibeMathedMath problems solved with AI
Sign in

The Sakoda-Sipser problem: exponential cost of simulating nondeterministic automata by two-way deterministic ones

Sakoda and Sipser (STOC 1978) asked how many states a two-way deterministic finite automaton (2DFA) needs to simulate an nn-state one-way or two-way nondeterministic automaton (1NFA, 2NFA). The best known simulations are exponential, and they showed that the family BhB_h (one-way liveness: words of binary relations on an hh-element set whose product is nonempty) is complete for the one-way case. Exponential lower bounds were known only for restricted deterministic targets (Sipser's sweeping automata, Kapoutsis's few-reversal machines), and against unrestricted 2DFAs only quadratic bounds were known. Is there a polynomial pp such that every nn-state 1NFA, or 2NFA, over any finite alphabet has an equivalent 2DFA with at most p(n)p(n) states?

Result
Disproved(see note)
Status
Candidate (review pending)
AI contribution
AI-discovered
Method
Argument
Field
Automata theory; descriptional (state) complexity
Posed by
William J. Sakoda and Michael Sipser
Year posed
1978
Years open
48y
Solved
2026-09-25
Model
Unreleased internal OpenAI model
Vendor
OpenAI
Collaborators
—
Verification
Lean-checked, statement unaudited
Publication
Announced
Collection
OpenAI math release (October 2026), version adc7f12
Significance
45 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

For every h≥2h\ge2, one-way liveness OWLh\mathrm{OWL}_h has a nondeterministic automaton with h+3h+3 states and no left moves, while every equivalent 2DFA with ss states satisfies 4(s+2)2≥2⌊(h−2)/31⌋4(s+2)^2\ge2^{\lfloor(h-2)/31\rfloor}. Hence no polynomial CncCn^c bounds 1NFA-to-2DFA (and so 2NFA-to-2DFA) conversion uniformly over finite alphabets. The deterministic target is unrestricted (stay moves, partial rules, infinite rejecting runs). The companion gives the weaker-rate bound 122⌊(n−4)/127⌋\tfrac12 2^{\lfloor(n-4)/127\rfloor} for the same family. Not shown: any lower bound over a fixed alphabet (e.g. binary), any bound in transition-table size, or anything about L versus NL.

What the AI did

The release README says every result in it was produced by an unreleased internal OpenAI model with a fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result, and that some outputs build on earlier model results. This result is not among the README's exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region). The manuscript is authored 'OpenAI' and names no human author. The principal manuscript (one-way liveness, September 25, 2026) and its companion on complementation (same date) are independent arguments; the complementation paper adapts the amplification pattern of the liveness paper and also yields a deterministic bound for the same family.

Verification

No independent mathematician has checked this yet. Checked here: Theorem 1.1 and Corollary 1.2 of the principal manuscript were read against the Sakoda-Sipser question. The witness is one-way liveness over the full relation alphabet, whose size grows with hh; the claim rules out an alphabet-independent polynomial bound, which is the usual (Kapoutsis) formulation of the problem, and it does not give a bound over a fixed alphabet or any logarithmic-space separation, as the paper says. lean/formalization.yaml lists a main result for this manuscript (comparator OneWayLiveness, declaration OAI.OneWayLiveness.main_theorem, file OAI/Combinatorics/Automata/Main.lean). ComparatorChallenges/OneWayLiveness.lean was read here: it defines deterministic machines with partial transitions, stay moves and endmarkers, two acceptance conventions, and states the existence of the (h+3)(h+3)-state no-left-move recognizer and the bound 2⌊(h−2)/31⌋≤4(s+2)22^{\lfloor(h-2)/31\rfloor}\le4(s+2)^2 (or 4(s+1)24(s+1)^2) for every deterministic recognizer. This states the headline. Not rebuilt here. Permitted axioms: propext, Quot.sound, Classical.choice.

Sources

Changelog1 change

Discussion