OpenAI model claims a proof of Khot's Unique Games Conjecture, with Lean formalization
Family 102 of OpenAI's 6 Oct 2026 math release, 'The Unique Games Theorem', claims a deterministic polynomial-time reduction from 3SAT to Unique Games over a fixed alphabet, with completeness ≥ 1 − ε and soundness ≤ δ. That would prove Subhash Khot's 2002 conjecture. Companion papers give direct proofs that Max-Cut is NP-hard beyond the Goemans–Williamson ratio and Vertex Cover NP-hard below factor 2. OpenAI formalized them in Lean; the community has not yet verified them.
Key facts
- Reactions: Joe Bebel, 'a claimed proof and Lean formalization of the Unique Games Conjecture, which I have been personally working on for the last year and a half' (~99k views); Chris Peikert: 'Unique Games Conjecture, proved. L=RL, proved.'
- Paper: 'The Unique Games Theorem' (dated 23 Sep 2026, 58 pages): for every fixed ε, δ ∈ (0, 1/2), a deterministic polynomial-time reduction from 3SAT to Unique Games over a fixed finite alphabet
- Companions: optimal Max-Cut hardness (beyond α_GW ≈ 0.878), Vertex Cover hardness below factor 2, constant-factor hardness for Min-UnCut and directed feedback vertex set, 'using established PCP and Label Cover hardness results'
- Lean: the scope note formalizes the reduction from binary 3SAT to unweighted bipartite unique games with alphabet 𝔽₂^s, the Max-Cut gap, the Vertex Cover threshold, Min-UnCut and DFVS; 'No assumption that P≠NP is built into the statement'
- Context: the 2-to-2 Games theorem (Khot–Minzer–Safra, 2018) was the strongest prior evidence; UGC implies optimal inapproximability for many problems
- The release also lists the 2-to-1 Games Conjecture with perfect completeness (family 105) and NP-hardness of colouring 3-colourable graphs with any constant number of colours (106)
Science result
- Field
- computer-science / computational complexity / hardness of approximation
- Problem
- Unique Games Conjecture (Khot 2002) (open since 2002)
- Result
- Claimed: NP-hardness of (1−ε, δ)-gap Unique Games for every fixed ε, δ; hence optimal NP-hardness for Max-Cut (Goemans–Williamson) and Vertex Cover (factor 2).
- AI system
- OpenAI internal model (unreleased)
- Human role
- Autonomous by OpenAI's fixed procedure (per README)
- Verification
- Lean formalization by OpenAI (review 'unchecked'); not yet expert-confirmed
- Status
- pending
- Why surprising
- UGC was among the best-known open conjectures in theoretical computer science.
What happened
OpenAI's release includes "The Unique Games Theorem", which claims a reduction from 3SAT to Unique Games. If valid, it proves the Unique Games Conjecture outright, with no reliance on unproven assumptions. A reasoning summary covers the related result on NP-hardness at the basic semidefinite threshold. Lean statements for all the hardness results are published as Comparator challenges.
Why it matters
UGC sits at the centre of hardness of approximation. A proof would make the Goemans–Williamson Max-Cut algorithm and the factor-2 Vertex Cover algorithm provably optimal unless P = NP. A formal proof makes checking faster, but encoding complexity-theoretic statements (machines, polynomial time, encodings) faithfully in Lean is subtle, and reviewers will need to check that the formal statement matches the conjecture.
Changelog
- 2026-10-07: added first expert reactions
- 2026-10-07: created from the openai/math repository
Related posts (2)
- TCS researcher: release includes a claimed, Lean-formalized proof of the Unique Games Conjecture he had worked on original ↗ Joe Bebel @joeintheory · x · 2026-10-06
First-hand reaction (~91k views) from a researcher working on the Unique Games Conjecture. - Explainer thread: the release's "4 biggest claims in plain English" (~203k views) original ↗ imjustnewatai @imjustnewatai · x · 2026-10-06
Most-viewed explainer thread; notes that none of the claims had been confirmed by outside mathematicians.
Related events
- OpenAI releases 722 AI-written math manuscripts (372 result families) claiming hundreds of open problems, incl. quasi-Riemann, Unique Games, Hodge for CM abelian varieties and free group factors ★★★★★
- The k-server conjecture, the 'holy grail' of online algorithms, is proved at Oxford; ChatGPT 6 Astra generalised the authors' k = 3 proof to all k ★★★★
Sources (6)
- discussionJoe Bebel on X
- discussionChris Peikert on X
- paperPaper: The Unique Games Theorem
- codeLean scope note for family 102
- codeComparator challenge: UniqueGamesTheorem.lean
- paperReasoning summary: NP-hardness at the basic semidefinite threshold
id: 2026-10-06-unique-games-conjecture-openai · updated 2026-10-07 · open in the interactive timeline