oai-math-revised beta

Browse › Theoretical computer science › 129 Exponential state costs for two-way automata

An exponential two-way deterministic state lower bound for one-way liveness

OpenAI · September 25, 2026

Lean

Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion

Edit NOTES.md · Existing issues · Source on GitHub

Abstract

One-way liveness on h points accepts a word of binary relations when their ordered product is nonempty. For every h ≥ 2, it has a nondeterministic automaton with $h+3$ states and no left moves, whereas every equivalent s-state two-way deterministic automaton satisfies $4(s+2)^2\ge2^{\lfloor(h-2)/31\rfloor}$. Partial transition rules, stay moves, and nonaccepting infinite computations are allowed. The alphabets are finite and grow with h, so the result rules out an alphabet-independent polynomial state bound for deterministic two-way simulation, already for one-way nondeterministic sources.

If the PDF does not display here, open it directly: Open PDF.

Notes

No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.

Automatically collected notes (unreviewed)

work in progress

Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.

Follow-up works

Formalization

  • OpenAI math release, Lean scope notes for family 129: Exponential state costs for two-way automata (lean/docs/129.md, October 2026). Describes the release's Lean formalization of the bound $2^{\lfloor(h-2)/31\rfloor}\le4(s+2)^2$ for every $h\ge2$ under both acceptance conventions; this paragraph follows a sentence excluding the one-way-liveness result from scope. [family-level]
  • OpenAI, OneWayLiveness.lean (OpenAI Math Release comparator statement, 2026). This file defines relation-product liveness and both finite-run acceptance conventions and states the small-source/exponential-target theorem, with its proof represented by a sorry placeholder.

Possibly relevant literature (found by the agent, not checked)

Elsewhere

Independent sites; their content is not reviewed here.

Cite

@misc{OAI:An-exponential-two-way-deterministic-state-lower-bound-for-one-way-liveness-September-25-2026,
  author = {{OpenAI}},
  title = {{An exponential two-way deterministic state lower bound for one-way liveness}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-exponential-two-way-deterministic-state-lower-bound-for-one-way-liveness-September-25-2026/main.pdf}{OAI:An-exponential-two-way-deterministic-state-lower-bound-for-one-way-liveness-September-25-2026}},
  year = {2026}
}

Lean formalization

OpenAI provides Lean files for this family: lean/docs/129.md. The Lean statements have not been checked by people against the paper's claims.

Family 129: Exponential state costs for two-way automata

Proves exponential lower bounds both for complementing two-way nondeterministic finite automata and for simulating one-way nondeterministic automata by two-way deterministic ones. The latter resolves the Sakoda–Sipser state-succinctness conjecture over growing finite alphabets; both results rule out polynomial state bounds independent of alphabet size.

Other papers in this family: