Lean formalization in OpenAI math repository (Result 104)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Randomized quasipolynomial-time mean-payoff games'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 104). The Lean development was not rebuilt locally.