Jump to content

The 2-to-1 Games Conjecture

From OpenAI Aftermath

The 2-to-1 Games Conjecture with perfect completeness, posed by Khot in 2002 together with the Unique Games Conjecture, asserts that for every fixed δ > 0 it is NP-hard to distinguish satisfiable 2-to-1 projection games (Label Cover instances) from games of value at most δ. A manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a proof, with a Lean formalization. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

Background

  • As recounted in the introduction of the manuscript:
    • A projection game has a bipartite multigraph of constraints, answer sets at its vertices and, for each edge, a map from the left answers to the right answers; its value is the largest fraction of edges a labeling can satisfy. In a 2-to-1 game the left alphabet has 2q answers, the right alphabet q, and every right answer has exactly two preimages under each map. Khot's original formulation allowed fibers of size at most two; the manuscript uses the exact-two convention. Perfect completeness means that on YES instances one labeling satisfies every constraint; hardness with completeness 1 − ε for each fixed ε > 0 does not give this endpoint. Ordinary repetition does not amplify the gap while keeping the games 2-to-1, since repeating an exact-two projection k times gives 2k preimages of every right answer.
    • Austrin, O'Donnell, Tan and Wright proved perfect-completeness hardness for 2-to-1 Label Cover with alphabets of sizes 6 and 3 and soundness 23/24 + ε.
    • The version with completeness arbitrarily close to one and arbitrarily small soundness came from the Grassmann and shortcode programme: the Grassmann-based reduction of Khot, Minzer and Safra, the reduction to a Grassmann agreement hypothesis by Dinur, Khot, Kindler, Minzer and Safra, the shortcode viewpoint of Barak, Kothari and Steurer, and the near-perfect expansion theorem of Khot, Minzer and Safra.
    • Fei, Minzer and Wang proved perfect-completeness hardness for 4-to-1 games at arbitrarily small fixed soundness. The manuscript cites their report ECCC TR26-179; the same authors posted arXiv 2610.12378v1 on 8 October 2026, which states Khot's d-to-1 conjecture with perfect completeness for every d ≥ 2 and proves the case d = 4. That version does not cite the OpenAI manuscript.
    • The manuscript notes that the uniformity condition of the Rich 2-to-1 framework of Braverman, Khot and Minzer is not part of its theorem.

The original result

  • Claim. Theorem 1.1 of the manuscript states that for every fixed rational δ ∈ (0, 1) there are an integer q = q(δ) ≥ 2 and a deterministic polynomial-time reduction from 3-SAT to 2-to-1 games with alphabets of sizes 2q and q such that satisfiable formulas give games of value 1 and unsatisfiable formulas give games of value at most δ. The output is a nonempty explicit list of unweighted edge occurrences with an explicit table for every projection map, each having exactly two preimages for every right answer; the degree and constants of the running-time bound may depend on δ. The manuscript's abstract states that it proves the 2-to-1 Games Conjecture with perfect completeness.
  • Method, as described: the external inputs are a perfect-completeness PCP gap, parallel repetition for projection games (Dinur and Steurer) and the Grassmann expansion theorem of Khot, Minzer and Safra, from which the manuscript derives inverse shortcode estimates following Barak, Kothari and Steurer. Copies of the questions of a clause-versus-variable game sit at the leaves of a finite rooted tree; each leaf carries all binary functions on its answer domain, each internal node the span of products of pairs of functions from its children, and a question is the partition of the leaf-answer domains by the joint values of lists of functions displayed at the nodes. Deleting one binary output direction merges at most two parts, giving preliminary constraints with fibers of size at most two that a satisfying assignment answers in full. For soundness, if a labeling satisfies a fixed positive fraction of these constraints, inverse shortcode estimates give product forms whose tested matrices have rank at most one; resampling arguments show that a positive part of the agreement comes from forms of bounded rank, which select short lists of source answers, and projection-game repetition gives the contradiction. A final step completes the maps to exact 2-to-1 maps and replaces rational edge weights by an explicit unweighted multiset.
  • Applications, as stated in the manuscript.
    • Corollary 1.2: for absolute constants C and k0 and every fixed k ≥ k0, it is NP-hard to distinguish k-colorable graphs from graphs in which every k-coloring properly colors at most a 1 − 1/k + C log k/k2 fraction of the edges. The manuscript obtains this from the reduction of Guruswami and Sinop, whose premise is the exact-two, perfect-completeness hypothesis, and describes their soundness bound as thereby unconditional.
    • Corollary 1.3: for every fixed 0 < ε < 3/8, satisfiable Not-Two instances are NP-hard to distinguish from instances in which every assignment satisfies at most a 5/8 + ε fraction of constraints, with the corresponding three-query PCP. The manuscript states that this recovers Håstad's unconditional theorem through the reduction of O'Donnell and Wu, and that it also follows from the 4-to-1 theorem of Fei, Minzer and Wang.
    • Through the reduction of Guruswami and Sandeep at d = 2, the theorem also recovers the hardness of distinguishing three-colorable graphs from graphs that are not c-colorable, which the manuscript attributes to Fei, Minzer and Wang (Corollary 1.7).
  • Source. The manuscript Perfect completeness for 2-to-1 games (23 September 2026).
  • Companion results in the collection. The manuscript Hardness of finding large independent sets in three-colorable graphs (24 September 2026) cites this theorem as supplying the perfect-completeness premise of Guruswami and Sandeep for d = 2, and proves a stronger independent-set form starting from ordinary projection Label Cover; see Hardness of coloring three-colorable graphs. The Unique Games Theorem mentions it in a footnote as a separate companion that is not an input to its own proof; see The Unique Games Conjecture.
  • Formalization, as described by the repository. The scope note lean/docs/105.md states that the formalization gives, for every fixed rational 0 < δ < 1, a deterministic polynomial-time reduction from binary 3SAT to nonempty unweighted games of value exactly 1 on satisfiable inputs and at most δ on unsatisfiable inputs, with exactly two preimages for each output label under each projection, an alphabet depending only on δ, and running time measured in the original input bit length. The Comparator statement is PerfectCompleteness.lean.
  • Catalogue status. A draft pull request to Google DeepMind's Formal Conjectures repository, #5430 (opened 10 September 2026, before the manuscript's date, and still a draft when checked on 19 October 2026), states the perfect-completeness 2-to-1 Games Conjecture as an open research problem (two_to_one_perfect), following the Label Cover convention of Guruswami, Khot, O'Donnell, Popat, Tulsiani and Wu with fibers of size at most two on equal alphabets.

Public follow-up work

Date Work Relation Public claim Public status (checked 19 October 2026)
2026-10-08 MathVet (GitHub, review of openai/math, tables at repository commit bb5fdb6, 18 October 2026) Review (fidelity of the formal statements) Rates the family "full". It notes that NP-hardness is encoded as a polynomial-time gap reduction from binary 3SAT in Mathlib's TM2 machine model, with the same encoding as the collection's Unique Games formalization, and that instances are multigraphs given as edge lists with repeats. It records a Comparator pass, run without a sandbox. MathVet states that its ratings concern whether the Lean states the headline claims.
2026-10-08 atimics/math2, Cross-family corollaries of openai/math, entry TC-1 (GitHub, commit 2c0f005) Use (conditional corollary) A written derivation (D) obtains hardness of 2-to-2 games with perfect completeness and arbitrarily small soundness from the manuscript's Theorem 1.1, by placing constraints between two copies of the left side that match the fibers of two exactly 2-to-1 maps. The entry states that this implication is already published, as the d = 2 case of Theorem A.3 of Dinur, Mossel and Regev applied to the manuscript's theorem. Repository catalogue (checked 19 October 2026); it states that every entry is conditional on the OpenAI claims it cites, that entries marked L are Lean-checked implications taking OpenAI's formal statement as a hypothesis and entries marked D are written derivations, and that the entries were rechecked by two independent agents.
2026-10-10 cert-machine, openai/math lane K, run 38074613260 (an earlier run, 38051470892, was terminated without a result) Verification (kernel replay) Records that Lean's default kernel accepts the PerfectCompleteness solution, while the nanoda kernel aborted with a stack overflow. The project's notes for the nanoda developers list this challenge among exports that overflow nanoda's fixed 16 MiB worker stack. Repository.
2026-10-10 to 2026-10-14 con-leche development journal (task #348) Verification (second kernel) In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions does not list PerfectCompleteness, so this challenge was accepted by con-leche and by Lean's official kernel. Development journal.

Notes

  • The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
Retrieved from "https://openai-aftermath.mathnt.net/index.php?title=The_2-to-1_Games_Conjecture&oldid=348"