Khot's 2-to-1 Games Conjecture with perfect completeness
A 2-to-1 game is a bipartite projection game with left alphabet and right alphabet in which every constraint map has exactly two preimages of each right label (Khot's original formulation allowed fibers of size at most two). Its value is the largest fraction of constraints satisfied by one labeling. Khot (2002) conjectured that for every there is a fixed alphabet size for which it is NP-hard to distinguish satisfiable 2-to-1 games from games of value at most . Khot, Minzer and Safra (2018) proved the version with completeness ; perfect completeness, which is what several coloring and satisfiable-CSP reductions need, was known only with soundness about (Austrin-O'Donnell-Tan-Wright), and Fei-Minzer-Wang had it for 4-to-1 games. Is it NP-hard, for every fixed , to distinguish satisfiable 2-to-1 games from those of value at most ?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Hardness of approximation; PCPs and label cover
- 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
- 45 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Claims Theorem 1.1: for every fixed rational there are and a deterministic polynomial-time reduction from 3-SAT to unweighted 2-to-1 games over with exact two-element fibers, value 1 on YES and at most on NO instances. Corollaries make the Guruswami-Sinop maximum -colorable subgraph hardness unconditional and recover Hastad's satisfiable Not-Two result. It does NOT prove the Rich 2-to-1 variant of Braverman-Khot-Minzer, the Unique Games Conjecture, or anything about alphabet size as a function of beyond existence.
What the AI did
The release README says the manuscripts were produced by an unreleased internal OpenAI model, the vast majority by one fixed procedure using on average about three hours of ChatGPT Pro thinking compute per result, and that some outputs build on earlier results produced by the models. Its named exceptions to that procedure (the zeta zero-free region work, whose Re(s) > 11/12 write-up was human edited, and the Hodge conjecture for CM abelian varieties) do not concern this family. The manuscript is credited to OpenAI with no human author named. Its external inputs are a perfect-completeness PCP, projection-game parallel repetition and the Khot-Minzer-Safra Grassmann expansion theorem, credited to their authors.
Verification
No independent mathematician has checked this yet. Theorem 1.1 was read against Khot's conjecture: for every fixed rational , a deterministic polynomial-time reduction from 3-SAT to exact 2-to-1 games over alphabets with value 1 on satisfiable formulas and at most otherwise. formalization.yaml lists ComparatorChallenges/PerfectCompleteness.json, declaration OAI.PerfectCompleteness.Theorem11.exists_reduction; the challenge JSON names solution module OAI.Computability.PerfectCompleteness.Main (present at the pinned commit). The statement was read here: for every rational there is a reduction with a fixed alphabet , projection tables with exactly two preimages per right label, a nonempty unweighted edge list, a TM2 machine computing it in polynomial time from a binary 3SAT encoding, value exactly 1 on satisfiable inputs and at most otherwise. That is the headline claim. Permitted axioms are propext, Quot.sound and Classical.choice. Not rebuilt here.