Khot's 2-to-1 Games Conjecture with perfect completeness

Claims Theorem 1.1: for every fixed rational $\delta\in(0,1)$ there are $q=q(\delta)$ and a deterministic polynomial-time reduction from 3-SAT to unweighted 2-to-1 games over $[2q],[q]$ with exact two-element fibers, value 1 on YES and at most $\delta$ on NO instances. Corollaries make the Guruswami-Sinop maximum $k$ -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 $\delta$ beyond existence.

Exact FrontierDelta

Prior state unknown→proved

Scope and record

Occurred: Sep 23, 2026

Delta type: SOURCE CLAIM

Assumptions: VibeMathed verification: lean-checked. Publication: announcement. AI contribution: ai-discovered. VibeMathed editorial classifications, scores, notes, relations, and dataset structure are CC BY 4.0. Source statements and linked content retain their own rights.

Canonical aliases: Khot's 2-to-1 Games Conjecture with perfect completeness · 2-to-1 Games Conjecture (perfect completeness)

Confidence: Not scored

Registry verification: lean checked · announcement · candidate

Open the source record ↗

Attribution

VibeMathed
registry · event recorded by

Unreleased internal OpenAI model
model · ai model contributor · OpenAI

Evidence vector

SourceReplayReproducedFormal proofStatement auditExternal checkExpert reviewPeer review

Named evidence

VibeMathed record: Khot's 2-to-1 Games Conjecture with perfect completeness

specialist registry · passed

No independent mathematician has checked this yet. Theorem 1.1 was read against Khot's conjecture: for every fixed rational $\delta\in(0,1)$ , a deterministic polynomial-time reduction from 3-SAT to exact 2-to-1 games over alphabets $[2q],[q]$ with value 1 on satisfiable formulas and at most $\delta$ 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 $0<\delta<1$ there is a reduction with a fixed alphabet $q\ge2$ , 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 $\delta$ otherwise. That is the headline claim. Permitted axioms are propext, Quot.sound and Classical.choice. Not rebuilt here.