Polynomial state complementation of two-way NFAs

Polynomial state complementation of two-way NFAs

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 129; 2026-09-25), the asserted result is that some $n$-state two-way nondeterministic automata require exponentially many states for recognizing their complements, when the alphabet may grow.

Mathematical statement of the claimed result

Manuscript 1.

For each $n\ge4$, let $H=[n-2]$ and alphabet $\Sigma_n=2^{H\times H}$. Compose relation letters in path order and define $L_H=\{R_1\cdots R_k:R_1\cdots R_k\ne\varnothing\}$, with the empty product the identity. The claim gives an $n$-state two-way nondeterministic finite automaton $A_n$ for $L_H$ and states \[ \text{states}(B)\ge\tfrac12\,2^{\lfloor(n-4)/127\rfloor}-1 \] for every two-way nondeterministic automaton $B$ recognizing $\Sigma_n^*\setminus L_H$. Machines have one read-only head, endmarkers and left/right/stay moves; acceptance requires a finite accepting run. The alphabet grows with $n$, so the theorem rules out a polynomial state bound uniform over finite alphabets.

Outline of the argument

For manuscript 1 (family 129; 2026-09-25), a small source automaton guesses a nonempty product of binary relations. Path diagrams of a hypothetical complement recognizer induce an order-reversing monoid image; corner reductions and a missing-set amplification force exponential rank loss and hence an exponential state bound.

Formal verification

For manuscript 1 (family 129; 2026-09-25), OpenAI lists Lean statements for this assertion: some $n$-state two-way nondeterministic automata require exponentially many states for recognizing their complements, when the alphabet may grow.

The selected statement includes the clause used for this problem.

The linked family Comparator checks are OneWayLiveness.lean, TwoWayComplementation.lean, TwoWayDeterminization.lean.

Their named declarations include OAI.OneWayLiveness.main_theorem, OAI.TwoWayComplementation.complementation_lower_bound_finite, OAI.TwoWayComplementation.explicit_family_main.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

• OpenAI, An exponential state lower bound for two-way nondeterministic complementation, 2026-09-25; citation key OAI:An-exponential-state-lower-bound-for-two-way-nondeterministic-complementation-September-25-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: main:theorem.
• Family 129: Lean scope.
• Comparator OneWayLiveness.json.
• Comparator OneWayLiveness.lean.
• Comparator TwoWayComplementation.json.
• Comparator TwoWayComplementation.lean.
• Comparator TwoWayDeterminization.json.
• Comparator TwoWayDeterminization.lean.
• OpenAI catalogue entry.