oai-math-revised beta

Browse › Theoretical computer science › 102 The Unique Games Conjecture and optimal approximation thresholds

The Unique Games Theorem

OpenAI · September 23, 2026

Lean

Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion

Edit NOTES.md · Existing issues · Source on GitHub

Abstract

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 δ.

If the PDF does not display here, open it directly: Open PDF.

Notes

No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.

Automatically collected notes (unreviewed)

work in progress

Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-23) and not checked by a person. May be wrong or incomplete. Report an error.

Follow-up works

  • Ariel Elboim, The Unique Games Theorem: A Short Self-Contained Proof (Zenodo, doi:10.5281/zenodo.23265572, version 1.0, 2026-10-09). An 11-page reconstruction of this paper's proof that takes Håstad's parity gap, the Khot–Minzer–Safra Grassmann expansion theorem and Dinur–Steurer repetition as inputs and simplifies the noise gadget, certificate extraction and decoding; it states no human expert has reviewed it. [AI-generated per source]
  • Ariel Elboim (@arielb42), post on X (2026-10-09). Thread announcing an 11-page self-contained version of the 58-page proof whose only cited inputs are Håstad's 3-LIN theorem, Khot–Minzer–Safra Grassmann expansion and Dinur–Steurer repetition.

Comments and discussion

  • Scott Aaronson, The Mathocalypse (Shtetl-Optimized, 2026-10-07). Relays Dana Moshkovitz's first reading of the release; her quoted messages note that it also contains "direct optimal NP hardness of approximation proofs" for the main applications of the UGC, bypassing the UGC. [family-level]
  • Dana Moshkovitz (relayed by Scott Aaronson), comment #2 on The Mathocalypse (Shtetl-Optimized, 2026-10-07). States the UGC "is true, though it wasn't really needed for the proof of its most famous corollaries", describes the proof's new tree-based recursive code with a noise test and the difficulty of reading it, and wonders whether a half-space code could also work.
  • Sasho Nikolov (@thesasho), post on X (2026-10-11). Describes the UGC proof as an extension of the Khot–Minzer–Safra line of work on the 2-to-1 games conjecture that "very much follows an existing program".

Formalization

  • OpenAI, Lean scope notes for family 102 (release Lean docs, lean/docs/102.md). States the formalized Unique Games gap reduction (binary 3SAT to unweighted simple bipartite fixed-alphabet translation games over F_2^s) and links the comparator statement UniqueGamesTheorem.lean. [family-level]
  • Ariel Elboim, unique-games-short-proof (lean_check) (GitHub, openai/math revision fd4aeeb, run 2026-10-09). Script and logs of an independent Comparator run on the release's Lean 4 formalization (Lean 4.34.1), reported as passing with only the three permitted axioms; it discloses unenforced sandboxing and no audit of the correspondence between formal statement and manuscript.
  • Henryk Michalewski, Formalize Unique Games, SSE, promise graph homomorphism and Gap-ETH (google-deepmind/formal-conjectures draft PR #5430, 2026-09-10). Adds a Lean statement of the Unique Games Conjecture as an open conjecture (not a proof); predates the release and does not reference it.

Possibly relevant literature (found by the agent, not checked)

Digests and expositions

News and blogs

Elsewhere

Independent sites; their content is not reviewed here.

Cite

@misc{OAI:The-Unique-Games-Theorem-September-23-2026,
  author = {{OpenAI}},
  title = {{The Unique Games Theorem}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-Unique-Games-Theorem-September-23-2026/paper.pdf}{OAI:The-Unique-Games-Theorem-September-23-2026}},
  year = {2026}
}

Lean formalization

OpenAI provides Lean files for this family: lean/docs/102.md. The Lean statements have not been checked by people against the paper's claims.

Family 102: The Unique Games Conjecture and optimal approximation thresholds

Proves Khot's Unique Games Conjecture. Independent direct reductions also establish NP-hardness, on unweighted graphs, of approximation beyond the Goemans–Williamson ratio for Max-Cut, below factor two for Vertex Cover, and within any fixed constant factor for Min-UnCut and directed feedback vertex set. These direct proofs use established PCP and Label Cover hardness results.

Other papers in this family: