AI Proved What?

Episode 104, October 2026

Who wins in the long run?

Claimed quasipolynomial algorithms for mean-payoff games, turn-based stochastic games and mean-payoff parity games

Covers result 104 in OpenAI’s catalog: all 4 papers. See its connections to other results and the work it cites.

7:10. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00Games that last forever
  2. 1:45The claims
  3. 3:46How the proof goes
  4. 6:34Where it stands

The claims, in plain words

In a mean-payoff game two players move a token around a directed graph forever. Max chooses the next edge at some vertices and Min at the others; every edge carries an integer weight, and the payoff of the infinite walk is its long-run average weight. Max wants that average to be at least zero. Ehrenfeucht and Mycielski showed that both players have optimal strategies depending only on the current vertex, so deciding the winner lies in NP ∩ co-NP. No polynomial-time algorithm is known.

The difficulty is the size of the weights. Zwick and Paterson’s algorithms take time polynomial in the number of vertices and in the largest weight, but a weight written with 60 binary digits is about 1018, so that time can be exponential in the length of the input. Björklund and Vorobyov’s randomized algorithm takes an expected 2O(√(n log n)) operations for n vertices. Parity games reduce to mean-payoff games with very large weights, and Calude, Jain, Khoussainov, Li and Stephan solved them in quasipolynomial time in 2017; that does not by itself handle general mean-payoff games.

Result 104 is four OpenAI preprints. The deterministic paper (27 pages) and the randomized paper (41 pages), dated September 25, 2026, compute the complete set of vertices from which Max can keep the average at least zero, using 2O((log L)²) bit operations for an input of length L: quasipolynomial, faster-growing than any polynomial but far slower than exponential. A reduction also gives the exact value at every vertex and optimal positional strategies for both players. The randomized algorithm is correct with probability at least 7/8, and a polynomial-time check certifies its answer. Two companions, dated October 5, extend the results: one (20 pages) finds the vertices of nonnegative value in turn-based stochastic mean-payoff games, deterministically and with the same bound, and so decides whether a simple stochastic game has value at least 1/2; the other (14 pages) solves mean-payoff parity games, using the deterministic algorithm as a subroutine.

What it doesn’t claim

The bounds are quasipolynomial, not polynomial; the deterministic paper calls a polynomial bound “a further improvement”. With constants set to one, at an input of a million bits a cubic bound has 19 digits, 2(log₂ L)² about 120, and 2L about 300,000: the claims are theoretical. The stochastic paper decides which vertices have nonnegative value; it does not compute values or strategies.

Where it stands

Posted as preprints
OpenAI, four preprints dated September 25 and October 5, 2026, released October 6
Peer reviewed
Not yet
Checked in Lean
In part: OpenAI published a Lean proof of the randomized algorithm’s winning-set theorem; we have not run the checks

Last checked October 19, 2026. The preprints have not been revised. OpenAI published a Lean formalization of the randomized algorithm’s winning-set theorem, 72 files and 17 more, about 27,000 lines, matched against its comparator statement: a Turing machine reading random bits that halts within 2C(log₂(L+2))² steps on every tape and is correct on at least 7/8 of them. It also formalizes a small counterexample from the randomized paper’s appendix to one variable-selection step of the claimed strongly polynomial tropical algorithm in Truffet’s arXiv version 4, within a model of that step; the appendix makes no claim about other versions. The deterministic, stochastic and parity results are not formalized, and we found no unproved steps in what is. We have not run the checks. None of the papers is among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

  1. Potentials in a wide box. Every weight w becomes (n + 1)w + 1, so no simple cycle sums to zero and a simple cycle’s new sum is positive exactly when its old sum is at least zero. A vertex’s update takes the best edge for its owner: the new weight plus the potential at the edge’s head. Clipped to a wide integer box, these updates have a unique fixed point whose coordinates fall into two bands: those near the top are exactly Max’s winning vertices, those near the bottom Min’s. Iterating to it can take about as many steps as the box is wide.
  2. Labels instead of the fixed point. Each vertex gets two positive masses, one per player. A Max witness is a potential at most its own update wherever it sits above the bottom of the box, on vertices of total mass at most one; wherever it comes near the top, the vertex must be labelled plus. Min witnesses are the mirror image. One labelling must satisfy every witness at once; with all masses 1/n the fixed point is a witness for both players, so a correct labelling is the winning set.
  3. The recursion. A pivot moves near the middle of the box, down and then up, guided by calls on boxes 128 times narrower. When a pass stops, every witness of the other type still needing labels has a set of mass more than 3/4 near its extreme. One call on a box half as wide labels those sets, and its labels reweight the masses by 4/5 or 8/5. Every child except the half-width one multiplies each product of a vertex’s two masses by at least 32/25; from 1/n² that happens only O(log n) times along a branch, so there are 2O((log L)²) calls.
  4. The companions. The stochastic paper replaces the long-run average by a discounted game, with a discount of polynomial bit length close enough to recover the exact set, and runs an adapted labelling. The parity paper adapts Parys’s recursion on dominions, with strategies that follow a mean-payoff strategy for longer and longer rounds between visits to a good priority.

The numbers in the video

  • A six-vertex game (Max owns 0, 2 and 4): brute force over positional strategies gives Max’s winning set {2, 4, 5}. From 4 the play settles on the cycle 2 → 5 → 2 with weights +2 and −2, average 0; from 0, Min keeps the play on 1 → 3 → 1, average −2.
  • The wide box has width 32,768; the fixed point is (0, 0, 32768, 1, 32768, 32755), with vertices 2, 4 and 5 at the top. The simple iteration takes 32,743 steps; with every weight multiplied by 10, 100 and 1,000 it takes 261,867, 2,094,355 and 16,749,219 steps, while the weights grow from 38 to 140 bits.
  • The recursion’s budget 1 + ⌊log32/25 n²⌋: 15 for 6 vertices, 56 for 1,000, 112 for a million.
  • A mean-payoff parity game where Max wins only with infinite memory (vertex a: reward 0, priority 1; vertex b: reward −1, priority 0): the increasing-round strategy averages −0.0139 after 104 steps and −0.0014 after 106.

Read the source

The 4 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Transcript

Read the full script

0:00Games that last forever

Two players push a token around a directed graph, forever. At the round vertices Max chooses the next edge; at the square ones, Min does. Each edge carries a whole-number weight, and the payoff of the infinite walk is its long-run average weight. Max wants that average to be at least zero; Min wants it negative. In this six-vertex game, starting here, the play settles into a cycle with weights +2 and −2, so the average tends to zero and Max wins. From this vertex, Min traps the play in a cycle averaging −2. Ehrenfeucht and Mycielski showed that both players have optimal strategies that depend only on the current vertex. Such a strategy is a short certificate, so deciding the winner lies in NP and in co-NP. No polynomial-time algorithm is known. The difficulty is the size of the weights. Zwick and Paterson gave algorithms whose time is polynomial in the number of vertices and in the largest weight. But weights are written in binary: a weight with 60 binary digits is about 10¹⁸, so their time can be exponential in the length of the input. In our example, a simple iteration took about 33,000 steps; multiplying every weight by 1,000 multiplied the steps by about 500, while the weights grew by only about 100 bits. Björklund and Vorobyov’s randomized algorithm takes an expected 2^(O(√(n log n))) operations, for n vertices. Parity games reduce to mean-payoff games with very large weights, and Calude, Jain, Khoussainov, Li and Stephan solved them in quasipolynomial time in 2017; that does not by itself handle general mean-payoff games.

1:45The claims

Result 104 is four OpenAI preprints. The first two, dated September 25, give a deterministic and a randomized algorithm for the complete set of vertices from which Max can keep the average at least zero. For an input of length L, each uses 2^(O(log² L)) bit operations. That is quasipolynomial: it grows faster than any polynomial, but far slower than exponential. A reduction also gives the exact value at every vertex, and optimal positional strategies for both players. The randomized algorithm is correct with probability at least 7/8, and a polynomial-time check certifies its answer. Two companions, dated October 5, extend the results. One finds the vertices of nonnegative value in turn-based stochastic mean-payoff games, where some moves are made by chance, deterministically and with the same bound. As a consequence, it decides whether a simple stochastic game, whose decision problem Condon placed in NP and co-NP, has value at least 1/2. The other solves mean-payoff parity games, which add a condition on which priorities recur, using the deterministic algorithm as a subroutine. For scale, with constants set to one, at an input of a million (10⁶) bits a cubic bound has 19 digits, this bound about 120, and 2^L about 300,000. The claims are theoretical. OpenAI published a Lean formalization of the randomized algorithm, 89 files and about 27,000 lines, in an explicit Turing-machine model. The deterministic, stochastic and parity results are not formalized. An appendix of the randomized paper gives a small counterexample to one step of a claimed strongly polynomial algorithm, in one version of a preprint by Truffet, also checked in Lean. We have not run the checks.

3:46How the proof goes

The proof works with potentials: one number per vertex. First, every weight w becomes (n + 1)w + 1. Then no simple cycle sums to zero, and each one’s new sum is positive exactly when its old sum is at least zero. Each vertex’s update takes the best edge for its owner: the weight plus the potential at the edge’s head. Clipped to a wide box, from 0 to D, these updates have a unique fixed point, and its coordinates fall into two bands: those near the top are exactly Max’s winning vertices, those near the bottom Min’s. In our game the box has width 32,768, and the fixed point puts vertices 2, 4 and 5 at the top, matching a brute-force check. But iterating to it takes about as many steps as the width. So the algorithm never computes the fixed point. It only decides which boundary each vertex is near. Each vertex gets two positive masses, one for each player. A Max witness is a potential that is at most its own update wherever it sits above the bottom of the box, on vertices of total mass at most one; wherever it comes near the top, the vertex must be labelled plus. Min witnesses are the mirror image. One labelling must satisfy every witness at once. With all masses 1/n, the fixed point is a witness for both players, so a correct labelling is exactly the winning set. The recursion moves a pivot near the middle of the box, first down and then up, guided by calls on boxes 128 times narrower. When a pass stops, any witness of the other type still needing labels has a set of mass more than 3/4 close to its extreme. One call on a box half as wide labels those sets, and the labels reweight the masses: lighter, by 4/5, where a vertex is labelled in a witness’s favor, and heavier, by 8/5, elsewhere. Every child call except the half-width one multiplies the product of each vertex’s two masses by at least 32/25. Starting from 1/n², that can happen only order log n times along any branch, so the number of calls is 2^(O(log² L)). The stochastic paper replaces the long-run average by a discounted game, with a discount of polynomial bit length that is close enough to recover the exact set, and runs an adapted labelling on the discounted update. The parity paper adapts Parys’s recursion on dominions, with strategies that follow a mean-payoff strategy for longer and longer rounds between visits to a good priority. In our example, where Max must visit a costly vertex infinitely often, the average of this strategy climbs toward zero: −0.0014 after a million steps.

6:34Where it stands

The four preprints are not peer reviewed and have not been revised. Lean covers the randomized algorithm and the counterexample; we have not run it. None of the papers is among those OSVerify reviewed, and we have seen no expert review. A polynomial-time algorithm would still be a further step. If the claims hold, the winners of mean-payoff games, of turn-based stochastic games and of mean-payoff parity games can all be found in quasipolynomial time, however large the weights.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.