Oct 6, 2026
Lean formalization in OpenAI math repository (Result 105)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'Perfect completeness for 2-to-1 games'. We prove the 2-to-1 Games Conjecture with perfect completeness. For every fixed rational \delta\in(0,1), it is NP-hard to distinguish satisfiable 2-to-1 games from games of value at most δ, with a fixed alphabet and an explicitly listed unweighted multiset of constraints.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 105). The Lean development was not rebuilt locally.