Polynomial deterministic two-way simulation of one-way NFAs

Polynomial deterministic two-way simulation of one-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 one-way relational liveness has small nondeterministic recognizers but exponentially large deterministic two-way recognizers, uniformly over the growing finite alphabets.

Mathematical statement of the claimed result

Manuscript 1.

For each $h\ge2$, use all binary relations on $[h]$ as letters and set \[ \operatorname{OWL}_h=\{R_1\cdots R_k:R_1\cdots R_k\ne\varnothing\}. \] Composition follows paths from left to right; the identity empty product makes the empty word accepted. The language is claimed recognizable by an automaton using nondeterministic transitions, $h+3$ states and only right or stay moves. By contrast, every deterministic two-way automaton recognizing it with $s$ states obeys \[ 4(s+2)^2\ge2^{\lfloor(h-2)/31\rfloor}. \] The target may use stay moves, partial transitions and nonaccepting infinite runs. If an accepting initial configuration counts as success, the sharper $s+1$ replaces $s+2$. The alphabet is not fixed independently of $h$.

Outline of the argument

For manuscript 1 (family 129; 2026-09-25), deterministic computations are represented by local matching diagrams and a sink tour. Composition passes to relation-monoid corners, where lifted permutations and rank-loss amplification bound the size of any image that separates live and empty products.

Formal verification

For manuscript 1 (family 129; 2026-09-25), OpenAI lists Lean statements for this assertion: one-way relational liveness has small nondeterministic recognizers but exponentially large deterministic two-way recognizers, uniformly over the growing finite alphabets.

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 two-way deterministic state lower bound for one-way liveness, 2026-09-25; citation key OAI:An-exponential-two-way-deterministic-state-lower-bound-for-one-way-liveness-September-25-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main, eq:main-bound.
• 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.