we-solve (beta)

CS-149 · computer science · mathematics · Algorithmic game theory

Deterministic quasipolynomial mean-payoff games

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
Do finite turn-based ordinary mean-payoff games with binary integer rewards admit deterministic quasipolynomial-time exact zero-threshold winning-set computation in the total binary input length?

Short English statement

Do finite turn-based ordinary mean-payoff games with binary integer rewards admit deterministic quasipolynomial-time exact zero-threshold winning-set computation in the total binary input length?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

CS-149-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for CS-149

The result supplies the conclusion in this problem with its displayed hypotheses and quantifiers. The broader statements and applications in the manuscript are kept separate from the particular question above. The supporting result is manuscript 1 (family 104; 2026-09-25). Other linked papers contribute only their stated special cases; those weaker results alone would not resolve the complete question.

Deterministic quasipolynomial mean-payoff games

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 104; 2026-09-25), the asserted result is that ordinary finite mean-payoff games have a deterministic quasipolynomial-bit-time solver for all zero-threshold vertices, exact values, and optimal positional strategies; In manuscript 2 (family 104; 2026-09-25), the asserted result is that ordinary mean-payoff games have a quasipolynomial-time randomized zero-threshold solver with success probability at least $7/8$ on every input and a polynomial certificate check.

Mathematical statement of the claimed result

Manuscript 1.
A finite directed arena, with each vertex assigned to Max or Min and binary integer edge weights, defines payoff $\operatorname{MP}_w(\pi)=\liminf_{T\to\infty}T^{-1}\sum_{t<T}w(e_t)$. Every vertex has a successor. For total binary encoding length $L$, the claimed uniform deterministic algorithm exactly returns \[ U=\{v:\exists\sigma\ \forall\tau:\operatorname{MP}_w(\pi_{v,\sigma,\tau})\ge0\} \] within $2^{C(\log_2(L+2))^2}$ bit operations for an absolute $C$. All preprocessing, exact arithmetic, recursion and output costs are counted. This is quasipolynomial, rather than polynomial, time.
Manuscript 2.
A finite directed Max/Min arena has at least one outgoing edge per vertex and binary integer edge weights. Let $\operatorname{MP}_w(\pi)=\liminf_{T\to\infty}T^{-1}\sum_{t<T}w(e_t)$. The claimed uniform randomized algorithm returns exactly \[ U=\{v:\exists\sigma\ \forall\tau:\operatorname{MP}_w(\pi_{v,\sigma,\tau})\ge0\} \] with probability at least $7/8$, using at most $2^{C(\log_2(L+2))^2}$ bit operations on every random tape, for an absolute $C$ and full binary input length $L$. The bound includes all preprocessing, recursion, arithmetic and random-bit generation. It is a randomized quasipolynomial algorithm, rather than a deterministic polynomial one.

Outline of the argument

For manuscript 1 (family 104; 2026-09-25), potential comparisons are encoded as simultaneous obligations on finite integer boxes. Recursion decreases both width and weighted support mass while protecting witnesses at moving boundaries; polynomially many threshold queries recover exact values and strategies.

For manuscript 2 (family 104; 2026-09-25), weighted potential supports are repeatedly transported and recentered in integer boxes. Random directions narrow the comparison bands while a decreasing rank ensures termination on every tape; verified positional strategies permit repetition with no erroneous accepted answer.

Formal verification

For manuscript 1 (family 104; 2026-09-25), the documented Lean scope is the randomized ordinary mean-payoff solver and a finite elimination counterexample at the family level; no selected declaration states the deterministic algorithm's full conclusion.

This coverage does not establish a formal proof of the complete problem as stated here.

For manuscript 2 (family 104; 2026-09-25), OpenAI lists Lean statements for this assertion: ordinary mean-payoff games have a quasipolynomial-time randomized zero-threshold solver with success probability at least $7/8$ on every input and a polynomial certificate check.

This coverage does not establish a formal proof of the complete problem as stated here.

The linked family Comparator checks are RandomizedMeanPayoff.lean, TruffetCounterexample.lean.

Their named declarations include OAI.TruffetV4Counterexample.finite_execution_not_optimal, OAI.randomized_quasipolynomial_mean_payoff.

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

Go to contribution →