Oct 6, 2026
Lean formalization in OpenAI math repository (Result 102)
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 'The Unique Games Theorem'. We prove the Unique Games Conjecture. For every fixed \varepsilon,\delta\in(0,1/2), we give a deterministic polynomial-time reduction from 3SAT to Unique Games over a fixed finite alphabet, with completeness at least 1-\varepsilon and soundness at most δ.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 102). The Lean development was not rebuilt locally.