Plectis Atlas
Search

↑ and ↓ move, Enter opens, Esc closes.

Show on the map

Quasipolynomial algorithms for mean-payoff, stochastic and parity games

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

Gives deterministic algorithms using \(2^{O((\log(L+2))^2)}\) bit operations, for complete binary input length L, for ordinary mean-payoff games and two separate extensions. They compute exact values and optimal positional strategies in ordinary games, the nonnegative expectation-of-liminf value set in turn-based stochastic games, and the winning set for nonnegative liminf mean payoff conjoined with parity. Signed rewards, rational chance probabilities, and parity priorities are unrestricted and binary-encoded. (OpenAI’s Lean note)

Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.

The independent assessments find that the Lean statements express only part of the result described above, or a narrower statement. Read the assessments

The paper states

Theorem 1.1

In Turn-Based Stochastic Mean-Payoff Games in Deterministic Quasipolynomial Time, 5 October 2026

Possible match to OpenAI’s description, selected from the papers’ main statements because it shares the most wording. No review confirming the selection is recorded.

Three other possible matches are listed below the card, among them Theorem 1.1 in Deterministic quasipolynomial-time mean-payoff games and Theorem 1.1 in Mean-payoff parity games in quasipolynomial time.

There are a uniform deterministic Turing machine and an absolute constant C such that, on every valid input described above, the machine outputs exactly U in at most

2^{C(\log_2(L+2))^2}

bit operations. The bound includes input reading, exact rational arithmetic, and output. Vertices of value zero are included.

No Lean statement in the release is paired with this theorem.

Three more possible matches

  • Theorem 1.1 in Deterministic quasipolynomial-time mean-payoff games.
  • Theorem 1.1 in Mean-payoff parity games in quasipolynomial time, 5 October 2026.
  • Theorem 1.1 in Randomized quasipolynomial-time mean-payoff games.
Reported proof verification
Two Lean statements in the release; independent groups report that Comparator accepted runs for all these files at the version shown here.
Papers and explanations
Four current papers, each readable here as a page beside its PDF.

Papers

Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.

Turn-Based Stochastic Mean-Payoff Games in Deterministic Quasipolynomial Time

5 October 2026, current edition.

Read it herePDF

We give a uniform deterministic quasipolynomial-time algorithm for finite turn-based stochastic mean-payoff games with signed integer rewards and rational chance-transition probabilities encoded in binary. It computes exactly the vertices of nonnegative value, including value zero, for the expectation of the pathwise liminf mean payoff. The algorithm uses exact rational arithmetic and \(2^{O((\log(L+2))^2)}\) bit operations, where L is the complete binary input length.

Mean-payoff parity games in quasipolynomial time

5 October 2026, current edition.

Read it herePDF

We give a uniform deterministic quasipolynomial-time algorithm for mean-payoff parity games. It computes all vertices from which a player can enforce both nonnegative liminf mean payoff and the parity condition, with arbitrary signed binary rewards and unrestricted binary priorities. The running time is \(2^{O((\log(L+2))^2)}\) bit operations, where L is the complete input length.

Deterministic quasipolynomial-time mean-payoff games

Undated, current edition.

Read it herePDF

We give a deterministic algorithm that computes the complete zero-threshold winning set of a finite mean-payoff game with arbitrary signed integer edge weights encoded in binary. For total explicit input length L, it uses \(2^{O((\log(L+2))^2)}\) bit operations. A reduction also computes the exact rational value at every vertex and globally optimal positional strategies for both players within the same quasipolynomial bound.

Randomized quasipolynomial-time mean-payoff games

Undated, current edition.

Read it herePDF

We give a randomized algorithm that computes the complete zero-threshold winning set of a finite mean-payoff game with arbitrary signed integer edge weights encoded in binary. For total explicit input length L, it uses \(2^{O((\log(L+2))^2)}\) bit operations on every random tape and is correct with probability at least 7/8. A polynomial-time check certifies the winning regions and positional strategies for both players or reports failure. Independent repetition therefore gives an always-correct algorithm with the same expected quasipolynomial bit bound.

Two Lean statements in this family

Choose one to see it beside the paper theorem it is paired with.

For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.

RandomizedMeanPayoff

The paper states

Theorem 1.1

In Randomized quasipolynomial-time mean-payoff games

There is a uniform randomized algorithm that, for every such game, returns the entire set

U=\{v\in V:\text{there is a Max strategy }\sigma \text{ such that for every Min strategy }\tau,\ \operatorname{MP}_w(\pi_{v,\sigma,\tau})\ge0\}

correctly with probability at least 7/8. For an absolute constant C>0, on every random tape its total cost is at most

2^{C(\log_2(L+2))^2}

bit operations in a standard model polynomially equivalent to a uniform probabilistic Turing machine. The bound includes preprocessing, recursive calls, intermediate arithmetic, and random-bit generation.

The words they share: pi, randomized, total, machine, random, tape, game, strategy, max, bit, quasipolynomial, payoff, mean, 7/8, probability, least, algorithm.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Randomized quasipolynomial mean-payoff algorithm

RandomizedMeanPayoff.lean, the release lists it as a main result.

noncomputable def MainClaim : Prop := by  classical  exact ∃ M : Machine, ∃ C : ℝ, 0 < C ∧ ∀ G : Game, ∃ T : ℕ,    (T : ℝ) ≤ (2 : ℝ) ^ (C * (Real.logb 2 ((input G).length + 2)) ^ 2) ∧    (∀ bits : Fin T → Bool, (result M G T bits).control = none) ∧    7 * 2 ^ T ≤ 8 * (Finset.univ.filter      (fun bits : Fin T → Bool => CorrectOutput G (result M G T bits))).cardtheorem randomized_quasipolynomial_mean_payoff : MeanPayoff.MainClaim := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

two independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.

Read the complete Lean statement

TruffetCounterexample

The paper states

Proposition 5.1 (Orientation)

In Randomized quasipolynomial-time mean-payoff games

Assume the lower-rank comparison guarantees stated at the beginning of this section. On a fixed permitted input (a,b;B,\alpha,\beta,k,m) of rank r, let (\chi,\mathcal H) be the output of \Orient. For every fixed admissible subsolution y of [a,b] whose core in Equation (5.1) satisfies \alpha(I_y)>\eta k,

\Pr\left( \chi=Y \ \text{or}\ \exists H\in\mathcal H: \alpha(S_y\cap H)>\eta k \right)\geq 1-\frac1{16}.

Separately, for every fixed admissible supersolution z of [a,b] with \beta(I_z)>\eta m,

\Pr\left( \chi=Z \ \text{or}\ \exists H\in\mathcal H: \beta(S_z\cap H)>\eta m \right)\geq 1-\frac1{16}.

On every tape, every set in \mathcal H has \mu-measure at most 1/2. Each probability statement remains valid conditional on a pre-call history that fixes its input and qualifying comparison, when the call uses fresh random bits.

The words they share: remains, stated, lower, output.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Finite counterexample to Truffet’s optimization procedure

TruffetCounterexample.lean, the release lists it as a supporting statement.

theorem finite_execution_not_optimal :    crossRowRestriction initial ∧    ForcedSingletonStep initial middle 0 1 ∧    ForcedSingletonStep middle finalState 1 0 ∧    (¬ ∃ j, finalState.remaining j) ∧ stop finalState ∧    feasible initial output ∧ feasible initial better ∧    output 2 = 0 ∧ better 2 = 0 ∧    (output 1 : Coeff) = eval (lowerForm initial 0 1) output ∧    (output 0 : Coeff) = eval (lowerForm middle 1 0) output ∧    eval initial.cost output = eval finalState.cost output ∧    eval initial.cost better < eval finalState.cost output := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program

  • cert-machine records it as “CERTIFIED”.
  • MathVet records it as “comparator-sandboxed-pass”.
  • Neal McBurnett, openai-math-lean-tooling records it as “accepted”.

Read the complete Lean statement

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.

MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.

MathVet finds that the Lean statements express a weaker statement than the advertised result (their term: “weaker-statement”).

Their note: Only a randomized (error 1/8) quasipolynomial algorithm for the winning set; the deterministic algorithm, exact values/optimal positional strategies, turn-based stochastic games and mean-payoff-parity games (two of four index papers) are not stated. TruffetCounterexample is a side negative result.

Definitions the group asks readers to compare with the paper: Custom 3-tape randomized Turing machine (structure Machine, step, run M code random, one random bit per step, alphabet Option Bool, heads in ℤ) with T existentially quantified per input and time = number of steps; standard in form but NOT Mathlib’s TM model, so ‘quasipolynomial bit time’ rests on this hand-rolled definition. Mean payoff is liminf of running averages and strategies are history-dependent (Strategy G := List (Fin G.m) →...), both standard

“weaker-statement”, in their words: The challenge statements do not imply the headline claim: they state a nontrivially weaker statement.

Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.

Read the original assessment Read MathVet’s method

cert-machine finds that the Lean statements express a narrower statement than the advertised result (their term: “NARROWER — UNDECLARED”).

The gap they name: Headline: deterministic quasipolynomial algorithms that compute values and optimal positional strategies (ordinary games), the nonnegative-value set of stochastic games, and mean-payoff-parity winning sets. Lean: one randomized (≥ 7/8 success) quasipolynomial algorithm for the zero-threshold winning set of ordinary games, plus a finite counterexample to Truffet’s procedure. Of the four manuscripts, only the randomized one is formalized.

“NARROWER — UNDECLARED”, in their words: The challenge statements state less than the headline, and OpenAI’s Lean note does not say so.

Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.

Read the original assessment Read cert-machine’s method

OpenAI’s own note on what its Lean covers

The formalization checks that a specified two-step execution of Truffet’s elimination procedure terminates with a feasible but nonoptimal output. It is a finite counterexample to that proposed optimization step.

The formalized result gives one randomized algorithm for the complete zero-threshold winning set of every finite mean-payoff game with signed binary weights. It succeeds with probability at least $7/8$ and runs in quasipolynomial bit time on every random tape. Self-loops, parallel edges, and history-dependent strategies are allowed, and winning means a nonnegative liminf average payoff.

AI-drafted comparisons, with no recorded human review

  • Randomized quasipolynomial mean-payoff algorithm RandomizedMeanPayoff

    Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem of the randomised paper: a quasipolynomial randomised algorithm computing the full winning set of every finite mean-payoff game with success probability at least 7/8. The deterministic algorithm of the companion paper is outside this statement.

  • Finite counterexample to Truffet’s optimization procedure TruffetCounterexample

    Unreviewed AI draft: states a supporting result. States a finite counterexample to a variable-selection rule in Truffet’s proposed elimination procedure, discussed in the randomised paper’s comparison section. It is a side result, not a headline theorem.

Who ran the proof-verification program?

These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.

These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.

Randomized quasipolynomial mean-payoff algorithm RandomizedMeanPayoff

Two reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report

Finite counterexample to Truffet’s optimization procedure TruffetCounterexample

Three reports, all at the release’s recorded version.

Reported byTheir wordTheir accountDateOriginal report
cert-machine“CERTIFIED”Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.10 October 2026Original report
MathVet“comparator-sandboxed-pass”Re-run through Comparator in a sandboxed virtual machine: accepted.8 October 2026Original report
Neal McBurnett, openai-math-lean-tooling“accepted”Re-run through Comparator with Lean’s kernel: accepted (the check took 83 s).10 October 2026Original report

Other proofs and exact calculations

These reports examine claims in the papers using exact calculations for finite claims, independently of the release’s Lean proofs. Read each report for the exact claim it covers.

  • Randomized quasipolynomial-time mean-payoff games

    Reported by
    cert-machine
    Method
    Exact computation
    Their verdict
    “CERTIFIED” Exact code written independently from the paper confirms that the published object has the claimed property.
    What it covers
    “a finite component (the appendix side result, not the main theorem): on the printed two-variable instance the true minimum is exactly 0, while the substitution rule as formalised in the challenge is forced through x2 = h, x1 = h + 1 to value 1; all 13 conjuncts of finite_execution_not_optimal. Faithfulness of the formalisation to Truffet v4 is a reading, not decided.”
    Original report
    Their report

What these papers cite in the release, and what cites them

These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.

Within this family

Papers elsewhere in the release that this family’s papers cite

This family’s papers cite no paper elsewhere in the release.

Papers elsewhere in the release that cite this family’s papers

No paper elsewhere in the release cites this family’s papers.

Explain a result, compare statements or propose a correction

Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.

Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.

Offer to write an explanationCompare one Lean statement with its paper: TruffetCounterexample, RandomizedMeanPayoffSuggest a source attributionSuggest a change

What people have said

Commentary on this family by others, dated and credited. It is commentary, not a finding.

  • An unsigned public tier list, the OpenAI Math Tier List, classes it as a algorithm and rates its significance, if it holds up, as “Career-defining publication”. The page says that nothing on it is verified.

    Author not stated. Source

Questions awaiting review

Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.

Read the Lean statement against the paper

  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form
  • An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded. Open the form

Identify the theorem the catalogue describes

  • Family 104 The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means. Open the form

Address a question raised in an independent assessment

Compare the proposed paper and Lean matches

  • Family 104 Atlas records no review of whether each linked Lean statement and paper theorem mean the same thing. Open the form