∑math20

Theoretical computer science · Result 105

Perfect completeness for 2-to-1 games

1 paperLean

Proves Khot's 2-to-1 Games Conjecture with perfect completeness: for every fixed rational \(\delta\in(0,1)\), it is NP-hard to distinguish satisfiable games from games whose optimum is at most δ, on explicit unweighted instances. The alphabet depends only on δ, and every right-hand label has exactly two preimages under each constraint map.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Perfect completeness for 2-to-1 games

Perfect completeness for 2-to-1 games

OpenAI · September 23, 2026

We prove the 2-to-1 Games Conjecture with perfect completeness. For every fixed rational \(\delta\in(0,1)\), it is NP-hard to distinguish satisfiable 2-to-1 games from games of value at most δ, with a fixed alphabet and an explicitly listed unweighted multiset of constraints.

Read PDF Download Source

Cite
@misc{OAI:Perfect-completeness-for-2-to-1-games-September-23-2026,
  author = {{OpenAI}},
  title = {{Perfect completeness for 2-to-1 games}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Perfect-completeness-for-2-to-1-games-September-23-2026/paper.pdf}{OAI:Perfect-completeness-for-2-to-1-games-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalized result establishes perfect-completeness hardness for 2-to-1 games. For every fixed rational \(0<\delta<1\), a deterministic polynomial-time reduction from binary 3SAT produces a nonempty unweighted game of value exactly \(1\) on satisfiable inputs and at most \(\delta\) on unsatisfiable inputs. Each constraint projection has exactly two preimages for each output label. The alphabet depends only on \(\delta\), and the runtime is measured in the original input bit length.

Comparator links

ResultComparator statement
Perfect-completeness reduction for 2-to-1 gamesPerfectCompleteness.lean

Scope note on GitHub →