Mean-payoff games in quasipolynomial time
Mean-payoff games in quasipolynomial time concerns the complexity of solving two-player mean-payoff games on graphs with binary-encoded weights, a problem in NP ∩ coNP for which no polynomial-time algorithm is known, together with its stochastic and parity extensions. Four manuscripts in OpenAI's public mathematics collection (github.com/openai/math), dated 25 September and 5 October 2026, claim deterministic algorithms using 2O((log L)2) bit operations, for input length L, for ordinary mean-payoff games, turn-based stochastic mean-payoff games and mean-payoff parity games, and a randomized algorithm with the same bound. The collection includes a Lean formalization of the randomized algorithm and of a related counterexample. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introductions of the manuscripts:
- Ehrenfeucht and Mycielski proved positional determinacy of mean-payoff games, which places the threshold problem in NP ∩ coNP, and Zwick and Paterson gave pseudopolynomial algorithms and a reduction to simple stochastic games. Brim, Chaloupka, Doyen, Gentilini and Raskin, Dorfman, Kaplan and Zwick (corrected by Austin and Dell'Erba), and Kozachinskiy studied energy games; Björklund and Vorobyov proved a subexponential expected bound for strategy improvement.
- Parity games reduce to mean-payoff games, and Calude, Jain, Khoussainov, Li and Stephan gave a quasipolynomial algorithm for parity games; Daviaud, Jurdziński and Lazić gave a pseudo-quasipolynomial algorithm for mean-payoff parity games.
- For stochastic games, Shapley introduced discounted stochastic games, Condon placed the simple stochastic game threshold problem in NP ∩ coNP and Ludwig gave a randomized subexponential algorithm; Andersson and Miltersen proved polynomial-time equivalences among simple stochastic, stochastic mean-payoff and stochastic discounted games.
The original results
- Claim. Theorem 1.1 of Deterministic quasipolynomial-time mean-payoff games states that a uniform deterministic algorithm returns the set of vertices from which Max can force a nonnegative mean payoff, using at most 2C(log2(L+2))2 bit operations; the manuscript also derives exact values, optimal positional strategies and minimum energy credits within the same bound. Theorem 1.1 of Randomized quasipolynomial-time mean-payoff games gives a randomized algorithm with the same bound that is correct with probability at least 7/8. Theorem 1.1 of Turn-Based Stochastic Mean-Payoff Games in Deterministic Quasipolynomial Time decides the set of vertices of nonnegative value in turn-based stochastic mean-payoff games, and the manuscript derives that deciding whether the value of a simple stochastic game is at least 1/2 is possible in the same time. Theorem 1.1 of Mean-payoff parity games in quasipolynomial time gives the winning set for nonnegative mean payoff conjoined with a parity condition.
- Method, as described: after a perturbation making every simple cycle sum nonzero, integer potentials are sought in a box through sub- and supersolutions of the game operator; a recursive simultaneous labeling procedure, whose branching occurs only logarithmically often along any path, shrinks the box, and the stochastic case applies a discounted version of the procedure with an explicit discount. The parity manuscript reduces its objective to the deterministic mean-payoff theorem.
- Sources. The manuscripts Deterministic quasipolynomial-time mean-payoff games, Randomized quasipolynomial-time mean-payoff games, Turn-Based Stochastic Mean-Payoff Games in Deterministic Quasipolynomial Time and Mean-payoff parity games in quasipolynomial time at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalization gives one randomized algorithm for the complete zero-threshold winning set of every finite mean-payoff game with signed binary weights, succeeding with probability at least 7/8 and running in quasipolynomial bit time on every random tape, and separately checks that a specified execution of Truffet's elimination procedure terminates with a feasible but nonoptimal output, a finite counterexample to that optimization step. The deterministic, stochastic and parity results are not part of this scope. The Comparator statements are
RandomizedMeanPayoff.leanandTruffetCounterexample.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 20 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates this family "weaker statement": only the randomized algorithm for the winning set is stated, while the deterministic algorithm, exact values and strategies, stochastic games and mean-payoff parity games are not; the Truffet counterexample is a side result. It notes that the randomized Turing-machine model is defined by hand. It records sandboxed Comparator passes for TruffetCounterexample and RandomizedMeanPayoff. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-10 | cert-machine, openai/math lane K: TruffetCounterexample (run 38019899278) and RandomizedMeanPayoff (run 38051470892) | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept both solutions, in 62 s and 576 s. The project reports two-kernel certification of 398 of 416 challenges of the collection. | Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (tasks #348 and #352–#353) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, both checkers accepted TruffetCounterexample; for RandomizedMeanPayoff, Lean's official kernel accepted while con-leche stopped with exhausted reduction fuel, and the journal records that a later con-leche build accepts the challenge. |
Development journal. |
| 2026-10-13 | M. Colbrook and contributors, AIM — Open Applied Problems (GitHub), problem 491 | Catalogue | The collection records its problem 491, a polynomial-time algorithm for simple stochastic games, as partially solved: the stochastic manuscript gives a deterministic quasipolynomial algorithm for the reachability threshold, which is not polynomial, and the linked Lean scope does not cover it. | The status review is described as "an AI statement-level review of a published manuscript, not a fresh independent audit of its complete proof or a Lean kernel replay". The collection is not affiliated with the American Institute of Mathematics. |
| 2026-10-16 | J. Jardine, Lattice24, referee reviews of the deterministic manuscript, the stochastic manuscript and the parity manuscript in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | All three reviews report no gap. The review of the stochastic manuscript states that every step of the main proof was checked by hand and has no minor notes. The review of the deterministic manuscript, which read sections 1 to 7 and skimmed the energy and tropical applications, notes that the finite-box comparison facts are imported from the randomized companion, which the reviewer re-derived. The review of the parity manuscript notes that the result is only as sound as the deterministic theorem it imports. | Part of an audit of the collection's manuscripts that the audit describes as complete. The reviews are published under CC BY 4.0. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscripts.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.