we-solve (beta)

CS-114 · computer science · mathematics · Algorithmic game theory · Algorithms and data structures · Optimization

Polynomial Algorithms for Mean-Payoff Games and Linear Programming

Status Open · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
$\mathbb N$, $\mathbb Z$, $\mathbb Q$, $\mathbb R$, and $\mathbb C$ denote the natural numbers, integers, rationals, reals, and complex numbers, respectively. All additional parameters and hypotheses are specified in the question.
Statement recorded in the supplied source.
Does there exist a polynomial-time algorithm for solving mean-payoff games? Does there exist a strongly polynomial algorithm for linear programming?

Formulation references: [S1], [S2].

Short English statement

Does there exist a polynomial-time algorithm for solving mean-payoff games? Does there exist a strongly polynomial algorithm for linear programming?

Sources

Catalogue entry

Statement licence: CC-BY-SA-4.0 · Source file

Contributions 1

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

OpenAI claim summary for CS-114

The game algorithms have quasipolynomial bit complexity rather than polynomial complexity. Encoding a reachability game in the stochastic payoff setting retains that larger bound, and no strongly polynomial linear-programming theorem is obtained.

Polynomial Algorithms for Mean-Payoff Games and Linear Programming

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-10-05), the asserted result is that mean-payoff parity games with arbitrary signed binary rewards and priorities have deterministic quasipolynomial-time winning-set computation; In manuscript 3 (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; In manuscript 4 (family 104; 2026-10-05), the asserted result is that finite stochastic games in which players move in turn admit deterministic quasipolynomial-bit-time zero-threshold solution for signed binary rewards and binary rational probabilities.

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 arena has an outgoing edge at every vertex, a Max/Min ownership partition, binary integer vertex rewards $r(v)$ and nonnegative integer priorities $p(v)$. For pure strategies Max's objective on $\pi=v_0v_1\cdots$ is \[ \min\{p(v):v\text{ recurs infinitely often}\}\text{ even},\qquad \liminf_{T\to\infty}T^{-1}\sum_{t<T}r(v_t)\ge0. \] The claimed deterministic, uniform algorithm decides for each vertex whether Max has a strategy forcing both conditions against every strategy of Min in at most $2^{C(\log_2(L+2))^2}$ bit operations, with absolute $C$ and full binary input length $L$. Priority count and reward magnitudes are unrestricted.
Manuscript 3.
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.
Manuscript 4.
Consider a finite explicitly encoded directed multigraph where every vertex has positive outdegree, integer edge rewards and vertices controlled by Max, Min or chance. Chance probabilities are binary rational numbers, and parallel edges, loops and zero probabilities are allowed. For behavioral strategies using the full history, define \[ \operatorname{MP}=\liminf_{T\to\infty}\frac1T\sum_{t<T}w(e_t),\qquad \operatorname{val}(i)=\sup_{\sigma}\inf_{\tau}\mathbb E_i^{\sigma,\tau}[\operatorname{MP}], \qquad U=\{i:\operatorname{val}(i)\ge0\}. \] The expectation follows the pathwise lower limit. The claim supplies a single deterministic Turing machine and absolute $C$ outputting exactly $U$ in \[ 2^{C(\log_2(L+2))^2} \] bit operations, where $L$ is the full binary input length, including exact rational arithmetic and output. Value-zero vertices are included.

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-10-05), the ordinary mean-payoff solver is coupled to attractor and bounded-dominion recursion. Uniform prefix-payoff bounds permit strategies to be combined across attractors, and a decreasing recursion budget bounds the full bit complexity.

For manuscript 3 (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. For manuscript 4 (family 104; 2026-10-05), rational gain separation reduces sign decisions to one discounted monotone fixed point. Simultaneous boundary labels move two nearby integer comparison vectors through shrinking boxes, reaching enough precision to include zero-valued vertices correctly.

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 3 (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.

No Lean formalization is listed at this snapshot for manuscript 2 (family 104; 2026-10-05), manuscript 4 (family 104; 2026-10-05).

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 →