The Unique Games Conjecture

A Unique Games instance is a graph with a finite label set $K$ and, on each edge, a permutation of $K$ ; a labeling satisfies an edge when the label at one endpoint is the image of the other endpoint's label under that permutation. Khot (2002) conjectured that for every $\varepsilon,\delta>0$ there is a finite alphabet size $q=q(\varepsilon,\delta)$ such that it is NP-hard to distinguish instances over $q$ labels in which a $1-\varepsilon$ fraction of the constraints can be satisfied from instances in which at most a $\delta$ fraction can. Under this hypothesis, optimal inapproximability was known for Max-Cut (the Goemans-Williamson ratio), Vertex Cover (factor $2$ ) and many other problems, but only conditionally. Is the Unique Games Conjecture true?

Result: Proved(see note)
Status: Candidate (review pending)
AI contribution: AI-discovered
Method: Argument
Field: Hardness of approximation, PCPs
Posed by: Subhash Khot, On the Power of Unique 2-Prover 1-Round Games, STOC 2002
Year posed: 2002
Years open: 24y
Solved: 2026-09-23
Model: Unreleased internal OpenAI model
Vendor: OpenAI
Collaborators: —
Verification: Lean-checked, statement unaudited
Publication: Announced
Collection: OpenAI math release (October 2026), version adc7f12
Significance: 74 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Theorem 1.1: for every fixed $\varepsilon,\delta\in(0,1/2)$ there are $s\ge1$ and a deterministic polynomial-time reduction from 3SAT to explicit unweighted, simple bipartite Unique Games over $K=\mathbb F_2^s$ whose constraints are translations $a(v)=a(u)+c_e$ , with value at least $1-\varepsilon$ on satisfiable formulas and at most $\delta$ on unsatisfiable ones. This is the conjecture in its usual edge-value form. The route keeps the Barak-Kothari-Steurer degree-two matrix shortcode and its Khot-Minzer-Safra inverse theorem and changes the noise through a nonlinear map to push completeness to $1-\varepsilon$ . Section 7 transfers known UG-hardness reductions (cut, covering, CSP, ordering, deletion, clustering) to NP-hardness; those reductions are credited to their authors. Companion manuscripts give direct NP-hardness proofs for Max-Cut beyond $\alpha_{GW}$ , Vertex Cover below factor $2$ , and every constant factor for Min-UnCut and directed feedback vertex set.

What the AI did

Produced by an unreleased internal OpenAI model as part of an OpenAI evaluation on open research problems. The release README says the vast majority of results used one fixed procedure, averaging about three hours of ChatGPT Pro thinking compute per result; this result is not among the README's stated exceptions (the Riemann zeta zero-free region work and the Hodge conjecture for CM abelian varieties). The manuscript is authored as OpenAI with no human author named. The README also cautions that unformalized results could have issues. The release also includes an abridged summary of the model's reasoning for this family (reasoning_traces/basic-semidefinite-threshold-np-hardness.pdf), and Lean formalizations of the main theorem and of the Max-Cut and Vertex Cover companions.

Verification

No independent mathematician has checked this yet. Checked here: the abstract, introduction and Theorem 1.1 of the principal manuscript, read against Khot's conjecture as cited (Khot 2010 survey, Conjecture 2.5; translation form via KKMO Corollary 13). The proof was not refereed. Lean: formalization.yaml lists OAI.UniqueGamesTheorem.theorem11 (lean/OAI/Computability/UniqueGames/Theorem.lean, comparator ComparatorChallenges/UniqueGamesTheorem.lean). Its statement was read: for all real 0 < eps, delta < 1/2 there is a reduction from binary-encoded 3SAT to nonempty simple bipartite translation Unique Games over a fixed alphabet identified with F_2^s, computable in polynomial time by a Mathlib TM2 machine, with completeness at least 1-eps and soundness at most delta. That is the headline claim, with no extra hypotheses; permitted axioms are propext, Quot.sound and Classical.choice. Not rebuilt here. The Max-Cut and Vertex Cover companions also have Lean main results (OAI.OptimalMaxCut.main, OAI.VertexCover.every_fixed_factor_below_two) whose statements match their headlines; also not rebuilt. The paper names Hastad's parity hardness and the Khot-Minzer-Safra Grassmann expansion theorem as external inputs; since theorem11 carries no hypotheses, a passing comparator check would mean those inputs are formalized too, which was not audited here.

The Unique Games Conjecture

What was actually shown

What the AI did

Verification

Sources

Discussion