AI Proved What?

Episode 102, October 2026

Unique Games, solved?

A claimed proof of Khot’s Unique Games Conjecture, and direct hardness proofs for four approximation problems

Covers result 102 in OpenAI’s catalog: all 5 papers. See its connections to other results and the work it cites.

Play Episode 102: Unique Games, solved? A small unique game on eight vertices with two-bit labels, all constraints satisfied but one.

7:15. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00Unique games
  2. 2:19The claims
  3. 4:02How the proof goes
  4. 6:33Where it stands

The claims, in plain words

A unique game labels the vertices of a graph from a fixed finite alphabet; each edge carries a permutation constraint, so a label at one end allows exactly one label at the other. Its value is the largest fraction of constraints one labeling satisfies. When every constraint can be satisfied, a labeling is easy to find: fix a label at one vertex, follow the constraints, and try each starting label. In 2002 Khot conjectured that the nearly satisfiable case is hard: for all ε, δ > 0, some fixed alphabet makes it NP-hard to tell games of value at least 1 − ε from games of value at most δ.

Assuming the conjecture, Khot, Kindler, Mossel and O’Donnell showed that Goemans and Williamson’s Max-Cut ratio αGW ≈ 0.8786 is optimal; Khot and Regev showed Vertex Cover would be hard below factor 2; and Raghavendra showed a basic semidefinite program would give the optimal ratio for every constraint satisfaction problem. Algorithms by Trevisan, by Charikar, Makarychev and Makarychev, and by Arora, Barak and Steurer (in subexponential time), and Khot and Vishnoi’s integrality gaps, showed how delicate the quantifiers are. In 2018 Khot, Minzer and Safra proved the 2-to-2 games theorem through Grassmann expansion, building on work with Dinur and Kindler and on Barak, Kothari and Steurer’s matrix formulation; it gave unique games hardness with completeness near 1/2.

Result 102 is five OpenAI preprints dated September 23, 2026. The main paper (58 pages) claims the conjecture: for every ε, δ in (0, 1/2), a deterministic polynomial-time reduction from 3SAT to unique games over a fixed alphabet F2s, on simple bipartite graphs with translation constraints, of value at least 1 − ε for satisfiable formulas and at most δ for unsatisfiable ones. Through the earlier conditional reductions, the thresholds above become NP-hard to beat for deterministic polynomial-time algorithms. Four companions prove some consequences directly, without the main theorem, from established hardness (the PCP theorem and label cover; the 2-to-1 games theorem for two of them): Max-Cut beyond αGW (38 pages), Vertex Cover below factor 2 (25 pages), Min-UnCut within any constant factor (38 pages) and directed feedback vertex set within any constant factor (29 pages).

What it doesn’t claim

The approximation consequences come from earlier reductions by the authors cited; the papers supply their hypothesis or prove some of them directly. The hardness rules out deterministic polynomial-time algorithms unless P = NP. A further companion on 2-to-1 games with perfect completeness is result 105 and is not an input to the main proof.

Where it stands

Posted as preprints
OpenAI, five preprints dated September 23, 2026, released October 6
Peer reviewed
Not yet
Checked in Lean
OpenAI published Lean proofs of all five main theorems; we have not run the checks

Last checked October 19, 2026. The preprints have not been revised. OpenAI published Lean formalizations of all five main theorems, about 1,800 files and 750,000 lines, with no unproved steps that we could find. The unique games development, 478 files and 186,782 lines matched against its comparator statement, also proves its inputs: the Khot–Minzer–Safra expansion theorem, the starting parity hardness through a PCP construction, and parallel repetition. We have not run the checks. None of the papers is among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

  1. The obstacle: completeness. In the matrix formulation a label is read off a binary matrix M as Mz, and the test adds a random rank-one matrix al⊤; the answer survives with probability (1 + 2−ℓ)/2, near one half. The new ingredient is a latent alphabet gadget: a larger space V containing the label space K, a nonlinear map C : V → K commuting with translations by K, and a noise law that changes C’s output with probability at most p, while linear observations of large rank on K still detect the noise with probability at least 1/8. It is built from quadratic blocks over a finite field, iterated with a rank potential.
  2. Completeness and soundness. The reduction starts from Håstad’s hardness for nearly satisfiable three-variable parity equations. Tables are affine maps into V, keyed so a table and its projections share answers, and folding makes every constraint a translation. For satisfiable formulas the test passes with probability at least 1 − p/2 on each satisfied tuple. For soundness, a labeling that passes 99% of the time has Fourier weight on low-rank frequencies, so it passes the ordinary rank-one test with fixed positive probability, and an inverse theorem derived from Grassmann expansion gives agreement with an affine evaluation on a slice.
  3. The contradiction. Two strategies for a repeated parity game, one sampling from short answer lists and one decoding with Fourier analysis, agree with probability bounded below independently of k. Sparse random questions leave many clean coordinates, where parallel repetition bounds success by e−c k1/3; for unsatisfiable formulas this is a contradiction. Removing weights and repeated edges, and a last round of parallel repetition, give explicit simple games with soundness at most δ.

The numbers in the video

  • A random unique game with 3,000 vertices, 8 labels and translation constraints: following a spanning tree recovers a perfect labeling when all constraints can be satisfied; with 5% of the constraints corrupted, it keeps about 74% on average, though a 95% labeling exists. A local search finds that labeling on these random examples; they are not hard instances.
  • Under a random rank-one update, the evaluation Mz keeps its value with probability (1 + 2−ℓ)/2: about 0.53 with 4 rows, 0.50 with 8 (simulated).
  • The Goemans–Williamson constant: αGW = min 2 arccos ρ / (π(1 − ρ)) ≈ 0.878567, at ρ ≈ −0.689.

Read the source

The 5 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Transcript

Read the full script

0:00Unique games

A unique game is a labeling puzzle. Each vertex of a graph gets a label from a fixed finite alphabet, and each edge carries a constraint that is a permutation: whatever label one end gets, exactly one label at the other end satisfies it. The value of the game is the largest fraction of constraints that one labeling can satisfy. If every constraint can be satisfied, finding such a labeling is easy: fix a label at one vertex and follow the constraints, trying each starting label until one works. In our example with 3,000 vertices and 8 labels, following a spanning tree recovers a perfect labeling. Corrupt 5% of the constraints, and the same method keeps only about 74% on average, although a labeling satisfying 95% still exists. A smarter local search finds it on random examples like this one; the question is whether every nearly satisfiable game is that easy. In 2002, Khot conjectured that it is not: for every pair of small errors, some fixed alphabet makes it NP-hard to tell games of value at least 1 − ε from games of value at most δ. Its importance is what it implies. Assuming it, Khot, Kindler, Mossel and O’Donnell showed that the Goemans–Williamson algorithm for Max-Cut, with ratio about 0.879, is optimal. Khot and Regev showed that Vertex Cover would then be hard to approximate within any factor below two, and Raghavendra showed that a basic semidefinite program would then give the optimal ratio for every constraint satisfaction problem. Several algorithms showed that the order of the quantifiers matters: Trevisan’s, Charikar, Makarychev and Makarychev’s, and Arora, Barak and Steurer’s, which runs in subexponential time. Khot and Vishnoi built games that fool semidefinite programs. In 2018, Khot, Minzer and Safra completed the proof of the 2-to-2 games theorem, through an expansion theorem for Grassmann graphs, building on joint work with Dinur and Kindler and on Barak, Kothari and Steurer’s matrix formulation. That gave hardness for unique games when the satisfiable side has value near 1/2, not near 1.

2:19The claims

Result 102 is five OpenAI preprints, all dated September 23. The main one, 58 pages, claims the conjecture itself. For every pair of errors ε and δ below 1/2, a deterministic polynomial-time reduction from 3SAT produces unique games over a fixed alphabet of binary vectors. The graphs are simple and bipartite, every constraint is a translation, and the value is at least 1 − ε when the formula is satisfiable and at most δ when it is not. Plugged into the earlier conditional reductions, this makes their thresholds NP-hard to beat: Max-Cut beyond Goemans–Williamson, Vertex Cover below two, Raghavendra’s thresholds, ordering problems and more. Four companions prove some consequences of the conjecture directly, without the main theorem, from established hardness results, including, for Max-Cut and feedback vertex set, the 2-to-1 games theorem. They cover Max-Cut beyond the Goemans–Williamson constant, in 38 pages; Vertex Cover below factor two, in 25; Min-UnCut, the fewest edges to delete to make a graph bipartite, within any constant factor, in 38; and directed feedback vertex set within any constant factor, in 29. OpenAI published Lean formalizations of all five, about 1,800 files and 750,000 lines in total. By our reading, the unique games formalization, about 187,000 lines, also proves its inputs, including the Khot–Minzer–Safra expansion theorem. We have not run the checks.

4:02How the proof goes

The obstacle is completeness. In the matrix formulation, a label is read off a binary matrix M as M times a fixed vector z, and the test adds a random rank-one matrix. The answer survives with probability one half plus a tiny bit: in our simulation, about 0.53 with 4 rows, and 0.50 with 8. That is why the earlier route stopped near 1/2. The new idea is a latent alphabet gadget: a larger space, a nonlinear decoding map C onto the label space, and a noise law. C commutes with translations by labels, and the noise changes C’s output with probability at most p, as small as one likes. Yet any linear observations of large enough rank on the label space still detect the noise at least 1 time in 8. The gadget is built from quadratic blocks over a finite field, iterated, with a rank potential. The reduction starts from Håstad’s hardness for nearly satisfiable parity equations on three variables. Proof tables are affine maps into the larger space, keyed so that a table and its projections share answers, and folding by translations makes every constraint a translation. If the formula is satisfiable, evaluating through C passes the test with probability at least 1 − p/2 on every tuple of equations that the parity assignment satisfies, giving completeness near 1. For soundness, a labeling that passes 99% of the time must put Fourier weight on low-rank frequencies, because high-rank ones are detected. That turns into passing the ordinary rank-one test with a small but fixed probability, where an inverse theorem, derived from Grassmann expansion, finds agreement with an affine evaluation on a slice. From those slices the paper builds two strategies for a repeated parity game: one samples from a short list of answers, the other decodes with Fourier analysis from its advice. Sparse random questions leave many clean coordinates, and on them, parallel repetition bounds the success by exp(−c k^(1/3)). For an unsatisfiable formula, that contradicts the decoded agreement once k is large. Finally, weights and repeated edges are removed, and one more round of parallel repetition brings the value for unsatisfiable formulas to at most δ, giving explicit simple games.

6:33Where it stands

The five preprints are not peer reviewed and have not been revised. Lean formalizations cover all five main theorems; we have not run them. None of the papers is among those OSVerify reviewed, and we have seen no expert review. A further companion, on 2-to-1 games with perfect completeness, is result 105. If it holds, the Unique Games Conjecture is a theorem, and a long list of approximation ratios, including about 0.879 for Max-Cut and two for Vertex Cover, cannot be beaten by any deterministic polynomial-time algorithm, unless P equals NP.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.