OpenAI claim summary for CS-147
computer sciencemathematicsTop Open Problemscontributionliterature_reportClaim: literature report
Summary of a claim published in openai/math; not a claim by this platform.
The displayed question has a negative answer under the manuscript's stated construction. Its counterexample meets the conditions in this problem and defeats the universal assertion, so this is a full disproof claim. The supporting result is manuscript 1 (family 129; 2026-09-25).
Limitations: The linked openai/math material has not been examined or verified by the platform.
Manuscript
Contents
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.