VibeMathedMath problems solved with AI
Sign in

Polynomial complementation of two-way nondeterministic finite automata

A two-way nondeterministic finite automaton (2NFA) has one read-only head moving in both directions between endmarkers. Deterministic two-way automata can be complemented with linearly many states (Geffert, Mereghetti and Pighizzini 2007), and Vardi (1989) complemented 2NFAs into exponential one-way automata. Kapoutsis (ICALP 2006) proved that small sweeping 2NFAs are not closed under complement, leaving unrestricted 2NFAs open. Is there a polynomial pp, independent of the alphabet, such that for every nn-state 2NFA over a finite alphabet the complementary language is recognized by a 2NFA 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
Open question in two-way automata state complexity; the manuscript cites it as open in Guillon, Prigioniero and Taheri (STACS 2026), after Kapoutsis's sweeping case (2006)
Year posed
—
Years open
—
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
25 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

Theorem 1.1: for every n≥4n\ge4 there is an nn-state 2NFA AnA_n for relation-product liveness on n−2n-2 points such that every 2NFA for its complement has at least 122⌊(n−4)/127⌋−1\tfrac12 2^{\lfloor(n-4)/127\rfloor}-1 states. Corollary: every 2DFA for the same language needs 122⌊(n−4)/127⌋\tfrac12 2^{\lfloor(n-4)/127\rfloor} states when n≥131n\ge131. The alphabet has 2(n−2)22^{(n-2)^2} letters, so the result says nothing about complementation over a fixed alphabet, about transition-table size, or about uniform logarithmic-space classes.

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 complementation manuscript (September 25, 2026) adapts the conjugate-amplification pattern of its companion on one-way liveness, but its transport and nested-class bounds are proved anew for nondeterministic path diagrams.

Verification

No independent mathematician has checked this yet. Checked here: Theorem 1.1 was read against the question; it is negative for alphabet-uniform polynomial complementation and, as the paper says, asserts nothing over one fixed alphabet. lean/formalization.yaml lists a main result for this manuscript (comparator TwoWayComplementation, declaration OAI.TwoWayComplementation.complementation_lower_bound_finite, file OAI/Combinatorics/TwoWayAutomata/Main.lean). ComparatorChallenges/TwoWayComplementation.lean was read here: for every n≥4n\ge4 it asserts an nn-state 2NFA over the alphabet of binary relations on n−2n-2 points such that every finite-state 2NFA recognizing the complement has at least 122⌊(n−4)/127⌋−1\tfrac12 2^{\lfloor(n-4)/127\rfloor}-1 states, with endmarkers, stay moves and finite-run acceptance. This states the headline. Not rebuilt here. Permitted axioms: propext, Quot.sound, Classical.choice.

Sources

Changelog1 change

Discussion