The Unique Games Conjecture
The Unique Games Conjecture is the subject of five manuscripts dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math). The conjecture, introduced by Khot in 2002, asserts that systems of permutation constraints can be hard to approximate even when almost all constraints can be satisfied; many optimal inapproximability thresholds had been proved assuming it. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original results
- Claim (Unique Games Theorem). For every fixed ε, δ ∈ (0, 1/2) there are an integer s ≥ 1 and a deterministic polynomial-time reduction from 3SAT to explicit unweighted Unique Games instances over the alphabet K = F2s, on simple bipartite graphs with translation constraints, such that satisfiable formulas give value at least 1 − ε and unsatisfiable formulas give value at most δ. The manuscript states that this resolves the conjecture positively in its usual edge-value formulation. Source: The Unique Games Theorem.
- Direct hardness results. Four further manuscripts give NP-hardness proofs that do not pass through the Unique Games Theorem and use established PCP and Label Cover hardness results: Max-Cut beyond the Goemans–Williamson ratio (A direct proof of optimal Max-Cut hardness), Vertex Cover below factor two (The factor-two hardness threshold for Vertex Cover), and Min-UnCut and directed feedback vertex set within every fixed constant factor (Min-UnCut, directed feedback vertex set).
- Consequences, as described in the manuscript. The Unique Games Theorem supplies the Unique Games hypothesis in earlier hardness reductions for cut, covering, constraint-satisfaction, ordering, deletion and clustering problems; the manuscript attributes those reductions and thresholds to their original authors (among them Khot, Kindler, Mossel and O'Donnell; Khot and Regev; Raghavendra).
- Formalization, as described by the repository. The scope note lean/docs/102.md states that the Lean formalization gives, for every fixed 0 < ε, δ < 1/2, a deterministic polynomial-time reduction from binary 3SAT to nonempty unweighted simple bipartite unique games with the stated completeness and soundness, over a fixed alphabet F2s with translation constraints; it also formalizes the Max-Cut, Vertex Cover, Min-UnCut and directed feedback vertex set results.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 14 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math at commit adc7f12, tables at repository commit cd0063d, 13 October 2026) |
Review (fidelity of the formal statements) | An independent, pre-referee review of whether each Lean statement says what the paper claims. Its per-family table rates this family "full", and its per-challenge table records Comparator passes for the five challenges: run in a sandbox for Vertex Cover and Min-UnCut, without a sandbox for the Unique Games and optimal Max-Cut challenges, and not yet run for directed feedback vertex set. | The review states that "full" means the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet. |
| 2026-10-09 | R. D. Barish, RBarish-UTokyo/Max3SAT-MaxSNP-APX-Lean4 (GitHub; Palomar PALOMAR-2026-10-09-000010, version 1) | Use (formal) | A Lean 4 proof of the PCP theorem (gap and verifier forms) and of MaxSNP- and APX-completeness of MAX-3-SAT and 3-occurrence MAX-3-SAT for an explicit single-tape Turing machine model. The registry record states that it includes 194 files of OpenAI's Unique Games formalization, adapted to the Lean module system. | Registered in the Palomar registry on 9 October 2026. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.