The Unique Games Conjecture and optimal approximation thresholds
OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:
Proves Khot’s Unique Games Conjecture. Independent direct reductions also establish NP-hardness, on unweighted graphs, of approximation beyond the Goemans–Williamson ratio for Max-Cut, below factor two for Vertex Cover, and within any fixed constant factor for Min-UnCut and directed feedback vertex set. These direct proofs use established PCP and Label Cover hardness results. (OpenAI’s Lean note)
Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.
Both independent assessments find that the Lean statements express or imply the whole result described above.Read the assessments
Possible match to OpenAI’s description, selected from the papers’ main statements because it shares the most wording. No review confirming the selection is recorded.
Seven other possible matches are listed below the card, among them Corollary 1.2 in The Factor-Two Hardness Threshold for Vertex Cover and Theorem 1.1 in A Direct Proof of Optimal Max-Cut Hardness.
For every fixed real constant A\ge1, it is NP-hard to approximate minimum directed feedback vertex set within factor A on unweighted digraphs. More precisely, there is a deterministic polynomial-time reduction from an NP-hard promise problem to instances (G,k) with k\in\N_{>0}. The polynomial and its constants may depend on A. The reduction has the following alternatives:
We prove the Unique Games Conjecture. For every fixed \(\varepsilon,\delta\in(0,1/2)\), we give a deterministic polynomial-time reduction from 3SAT to Unique Games over a fixed finite alphabet, with completeness at least \(1-\varepsilon\) and soundness at most δ.
Choose one to see it beside the paper theorem it is paired with.
For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
DirectedFeedback.lean, the release lists it as a supporting statement.
defMainStatement : Prop := ∀ A : ℝ, 1 ≤ A → ∀ language : List Bool → Prop, InNP language → Nonempty (GapReduction A language)⋮theoremDirectedFeedback.main : DirectedFeedback.MainStatement := bysorry
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
Atlas has no report of an independent group using Comparator to verify OpenAI’s proof of this Lean statement at the version shown here. Who ran the proof-verification program
For every fixed integer K\ge2, there is a deterministic polynomial-time many-one reduction mapping a 3SAT formula \varphi to a pair (G,k), where G is an explicit finite simple undirected unweighted graph and k\ge1 is a binary-encoded integer, such that
For each fixed K, the graph size, full construction work, and bit complexity are polynomial in the bit length of \varphi. All constants are effective; no advice or oracle is supplied to the reduction.
The words they share: uncut, length, formula, bit, size, opt, satisfiable, finite, reduction, time, integer, polynomial, min, cut, encoded, one, unsatisfiable, sat, simple, unweighted, constants, deterministic.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
MinUncut.lean, the release lists it as a supporting statement.
theoremmain : Nonempty Reduction := bysorry
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
Atlas has no report of an independent group using Comparator to verify OpenAI’s proof of this Lean statement at the version shown here. Who ran the proof-verification program
For every fixed \varepsilon,\delta\in(0,1/2), there are an integer s\ge1 and a deterministic polynomial-time reduction from \mathrm{3SAT} to explicit unweighted Unique Games instances G_\varphi over K=\F_2^s such that
The graph is simple and bipartite, and every constraint is a translation a(v_e)=a(u_e)+c_e of K. The alphabet, the degree of the running-time polynomial, and its constants depend only on \varepsilon,\delta.
The words they share: alphabet, bipartite, constraint, depend, deterministic, explicit, fixed, games, instances, integer, polynomial, reduction, satisfiable, simple, theorem, time, translation, unique, unsatisfiable, unweighted.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
For every fixed integer m\geq4, there is a deterministic polynomial-time reduction from \mathrm{3SAT} to finite simple undirected unweighted graphs with the following guarantees:
\begin{array}{ll}
\text{the formula is satisfiable}
&\Longrightarrow\quad
\tau(G)<\left(\dfrac12+\dfrac1m\right)|V(G)|,\\[6pt]
\text{the formula is unsatisfiable}
&\Longrightarrow\quad
\tau(G)>\left(1-\dfrac1m\right)|V(G)|.
\end{array}
The output lists all vertices and edges explicitly.
The words they share: vertices, edges, cover, formula, explicit, sat, lists, gap, 1/2, satisfiable, graphs, finite, reduction, time, integer, two, factor, unsatisfiable, simple, unweighted, polynomial.
Possible Lean counterpart
Selected from shared wording. No review of whether the statements mean the same thing is recorded.
VertexCover.lean, the release lists it as a main result.
theoremexplicit_cover_gap (m : ℕ) (hm : 4 ≤ m) : Nonempty (GapReduction m) := bysorry
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
Other mathematical statements in OpenAI’s Lean library
Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.
Independent comparisons and proof-verification reports
Does the Lean express the advertised result?
MathVet and cert-machine agree on how much of the advertised result the Lean statements express.
MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.
MathVet finds that the Lean statements express or imply the whole advertised result (their term: “full”).
Their note:None found; all five hardness statements are formalized as polynomial-time (Mathlib TM2, finite stack alphabets) Karp gap reductions from binary 3SAT (or an arbitrary NP verifier language), which is the standard NP-hardness encoding. Cone is ~190k lines and uses ‘Std’/‘Lean’ (core) only; the OptimalMaxCut axiom_files flag is a comment-only false positive.
Definitions the group asks readers to compare with the paper:Complexity notions are Mathlib’s Turing.TM2ComputableInPolyTime (note: Mathlib’s FinTM2 only forces the input stack alphabet to be finite, so every challenge adds finiteAlphabet : ∀ k, Finite (computation.tm.Γ k)), outputs are measured in explicit unary/binary encodings (gameBits writes every number in unary); alphaGW is defined as an sInf over ρ ∈ [-1,1) (equals the GW constant, checked); InNP is the certificate definition via NPVerifier with a polynomial witnessBound
“full”, in their words: The challenge statements imply the headline claim after unpacking definitions or one routine step.
Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
The Unique Games conjecture asks for hardness of distinguishing nearly satisfiable unique games from games of very small value. The formalized result gives, for every fixed $0<\varepsilon,\delta<1/2$, a deterministic polynomial-time reduction from binary 3SAT to nonempty unweighted simple bipartite unique games. Satisfiable inputs have value at least $1-\varepsilon$ and unsatisfiable inputs have value at most $\delta$. The alphabet is a fixed $\mathbb F_2^s$ depending only on the errors, and every constraint is a translation.
The formalized result establishes hardness of approximating Max-Cut beyond the Goemans–Williamson constant $\alpha_{\mathrm{GW}}$. For every fixed $\alpha_{\mathrm{GW}}<\alpha\le1$, it gives a deterministic polynomial-time reduction from binary 3SAT to a strictly separated Max-Cut gap on finite simple unweighted graphs. The reduction includes the explicit positive integer scaling used in the gap statement.
The formalized result gives the factor-two hardness threshold for Vertex Cover. For each integer $m\ge4$, a polynomial-time reduction from binary 3SAT produces simple unweighted graphs with cover density below $1/2+1/m$ on satisfiable inputs and above $1-1/m$ on unsatisfiable inputs. Consequently, any polynomial-time approximation with a fixed factor $1\le\alpha<2$ would give a polynomial-time decision algorithm for 3SAT. No assumption that $P\ne NP$ is built into the statement.
Min-UnCut minimizes the number of edges left uncut by a bipartition. The formalization constructs a deterministic reduction from encoded $3$-SAT formulas to finite simple unweighted Min-UnCut instances with arbitrarily large fixed multiplicative gaps. For every integer $K\ge2$, satisfiable formulas give optimum at most the output threshold, while unsatisfiable formulas give optimum strictly greater than $K$ times that threshold. Runtime and output length are polynomial for each fixed $K$, establishing hardness for every fixed approximation factor greater than one.
A directed feedback vertex set meets every directed cycle. The formalization proves hardness of approximating the minimum such set within any fixed constant factor. For every real factor $A\ge1$ and every language in NP, it constructs a polynomial-time gap reduction to unweighted directed graphs with the stated completeness and soundness separation. Thus a fixed-factor polynomial-time approximation would imply a polynomial-time algorithm for every NP language.
AI-drafted comparisons, with no recorded human review
Optimal Max-Cut hardness gapOptimalMaxCut
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem in reduction form: for every α above the Goemans–Williamson constant, a polynomial-time reduction from 3SAT to a separated Max-Cut gap on simple unweighted graphs, which is how NP-hardness of α-approximation is expressed.
Constant-factor hardness of directed feedback vertex setDirectedFeedback
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: for every factor A ≥ 1, a polynomial-time gap reduction from any NP language to directed feedback vertex set, so fixed-factor approximation would put NP in P.
Arbitrary constant-factor hardness of Min-UnCutMinUncut
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem: for every K ≥ 2, a polynomial-time reduction from 3SAT to Min-UnCut with multiplicative gap K. The 2CNF-deletion corollary is not part of the statement.
Unique Games gap reductionUniqueGamesTheorem
Unreviewed AI draft: states a paper’s theorem as the paper does. States the paper’s Unique Games theorem as a reduction: for fixed ε, δ in (0, 1/2), a deterministic polynomial-time reduction from 3SAT to translation unique games with completeness 1 − ε and soundness δ.
Vertex Cover gap and factor-two hardnessVertexCover
Unreviewed AI draft: states a paper’s theorem as the paper does. States the explicit cover-gap reduction for each m ≥ 4 and its corollary that approximation within any fixed factor below 2 would decide 3SAT in polynomial time.
Who ran the proof-verification program?
These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.
These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.
Optimal Max-Cut hardness gapOptimalMaxCut
Two reports, all at the release’s recorded version.
Reported by
Their word
Their account
Date
Original report
cert-machine
“REFUSED”
Re-run through Comparator did not reach a verdict (the job ended (failure) in the step "comparator, Lean’s kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.)).
Constant-factor hardness of directed feedback vertex setDirectedFeedback
One report, at the release’s recorded version.
Reported by
Their word
Their account
Date
Original report
cert-machine
“REFUSED”
Re-run through Comparator did not reach a verdict (the job ended (failure) in the step "comparator, Lean’s kernel and nanoda" without uploading a result: the runner terminated it (GitHub: The hosted runner lost communication with the server. Anything in your workflow that terminates the runner process, starves it for CPU/Memory, or blocks its network access can cause this error.)).
Arbitrary constant-factor hardness of Min-UnCutMinUncut
One report, at the release’s recorded version.
Reported by
Their word
Their account
Date
Original report
cert-machine
“REFUSED”
Re-run through Comparator did not reach a verdict (the job ended (failure) in the step "comparator, Lean’s kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.)).
Two reports, all at the release’s recorded version.
Reported by
Their word
Their account
Date
Original report
cert-machine
“REFUSED”
Re-run through Comparator did not reach a verdict (the job ended (failure) in the step "comparator, Lean’s kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.)).
Vertex Cover gap and factor-two hardnessVertexCover
Two reports, all at the release’s recorded version.
Reported by
Their word
Their account
Date
Original report
cert-machine
“REFUSED”
Re-run through Comparator did not reach a verdict (the job ended (failure) in the step "comparator, Lean’s kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.)).
Other people’s accounts of running proof-verification software, with links to their reports.
carlostoledo1891, def_eq unfolds proofs when proof irrelevance fails (issue 44), with a replay of every openai/math challenge, 11 October 2026. Source
Five family-102 challenges (UniqueGamesTheorem, DirectedFeedback, MinUncut, OptimalMaxCut, VertexCover) still overflow the 16 MiB stack even with the patch, though Lean’s kernel accepted them.
Robert Joseph George, Do the Lean statements in openai/math match their papers?, 7 October 2026. Source
The review reports that Comparator accepted OpenAI’s solution for this challenge, run end to end on Lean 4.34.1 with the default kernel and only the three standard axioms.
Explanations by others
Explanations of this family written elsewhere, by the people named. Each is their own reading of the mathematics.
Moshkovitz’s early assessment: the Unique Games conjecture is true by a new tree-based code with a noise test, though its famous corollaries (Max-Cut and other CSPs) have separate direct hardness proofs; the writeup is hard to read.
OfficeChai Team, OpenAI Releases AI-Generated Proofs Of Quasi Riemann Hypothesis, Unique Games Conjecture & Hodge Conjecture For CM Abelian Varieties, 7 October 2026. Source
A proof of Khot’s Unique Games Conjecture would make the known Max-Cut and Vertex Cover algorithms optimal unless P = NP.
Gil Kalai, Updates: Sharing AI progress on mathematics (amazing!); and my lecture plans, 7 October 2026. Source
Lists the Unique Games Theorem and the perfect-completeness 2-to-1 Games result among the items related to their earlier posts.
seaworld008, seaworld008/openai-math-top30: thirty selected families explained in Chinese, 7 October 2026. Source
Chinese-language explainer for general readers, with a beginner’s section, a specialist section, background on why the problem was hard and a diagram; it ends by saying it paraphrases OpenAI’s summary and does not represent consensus.
Missing or incomplete source records
The program that collects Atlas’s source records, Statement Map, could not obtain or interpret some source material. These notes describe those limits; they do not identify mathematical errors.
UniqueGamesTheorem: Tracked source lean/OAI/Computability/UniqueGames/Main.lean unavailable: bytes were not captured at fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb
What these papers cite in the release, and what cites them
These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.
Papers elsewhere in the release that this family’s papers cite
PALOMAR-2026-10-09-000010 (Robert Barish) reuses 194 files of the release’s Unique Games Lean library inside a PCP and MAX-3-SAT development.
Palomar registry, Palomar: a registry of Lean-verified mathematics, 9 October 2026. Source
RBarish-UTokyo’s MaxSNP and APX completeness of MAX-3-SAT reuses the 194-file Unique Games formalisation from the OpenAI repository (PALOMAR-2026-10-09-000010).
offline-ant, wiggums-proof-loop, 9 October 2026. Source
The Lean proof for the Unique Games result was reduced by about a quarter in line count by AI agents; the author reports a clean rebuild with only the standard axioms.
Robert D. Barish, MaxSNP-completeness and APX-completeness of MAX-3-SAT in Lean 4 (PALOMAR-2026-10-09-000010), 9 October 2026. Source
Registered 2026-10-09T11:47:04Z; provenance maps every adapted file to its upstream file in docs/PROVENANCE.md.
RBarish-UTokyo, RBarish-UTokyo/Max3SAT-MaxSNP-APX-Lean4: MaxSNP- and APX-completeness of MAX-3-SAT in Lean 4, 8 October 2026. Source
Lean proof of MaxSNP- and APX-completeness of MAX-3-SAT reusing the family 102 gap-amplification code.
From github.com/lgboim/unique-games-short-proof, 7 October 2026. Source
Commenter Ariel posted an 11-page self-contained presentation and a 17-page faithful presentation of the Unique Games proof, prepared with Codex and Claude, not yet human-reviewed.
Ben Brubaker, As AI Closed In on 'Unique Games’ Proof, Researchers Raced to Beat the Machines, 7 October 2026. Source
Minzer, Fei and Wang (human-written, posted mid-September) proved a four-options-per-constraint variant of Khot’s 2-to-1 games conjecture, implying hardness for colouring 3-colourable graphs with any constant number of colours.
References outside the release
Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release
Explain a result, compare statements or propose a correction
Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.
Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.
Commentary on this family by others, dated and credited. It is commentary, not a finding.
An unsigned public tier list, the OpenAI Math Tier List, classes it as a proof and rates its significance, if it holds up, as “Would win a Fields Medal”. The page says that nothing on it is verified.
From github.com/mahrud/openai-math-comments, 9 October 2026. Source
Points to arXiv:2610.12378, ECCC report 2026/179 and a Quanta article on the race to a Unique Games proof.
Scientific American (byline not recorded), The most exciting claims from OpenAI’s heap of new proofs, 8 October 2026. Source
The article reports that the Unique Games proof is controversial because other researchers rushed out partial progress for fear of being scooped by AI.
JohnDriscollAcademic, Significant Number of OpenAI Results Appearing to Resolve AIM Problems (issue 36), 7 October 2026. Source
AIM problem 293 (Unique Games Conjecture) corresponds to family 102.
Dana Moshkovitz, as relayed by Aaronson, finds the Unique Games proof very hard to read and notes that it builds a new tree-based code with a noise test rather than the long or short code, with the main hardness-of-approximation corollaries also proved directly without the conjecture.
Questions awaiting review
Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.
Run Comparator on OpenAI’s proof
Atlas records no independent report that Comparator accepted the proof at the release version shown here.Open the form
Atlas records no independent report that Comparator accepted the proof at the release version shown here.Open the form
Read the Lean statement against the paper
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
Identify the theorem the catalogue describes
Family 102The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means.Open the form
Address a question raised in an independent assessment
Atlas records no review confirming that the two statements mean the same thing.
Independent assessment
MathVet
Their term
“full”
What their term means
The challenge statements imply the headline claim after unpacking definitions or one routine step.
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.
The challenge statements state the headline as OpenAI wrote it.
Their method
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners…
Re-run through Comparator did not reach a verdict (the job ended (failure) in the step "comparator, Lean’s kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.)).
Date
10 October 2026
Version
at the release’s recorded version
Their method
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator did not reach a verdict (the job ended (failure) in the step "comparator, Lean’s kernel and nanoda" without uploading a result: the runner terminated it (GitHub: The hosted runner lost communication with the server. Anything in your workflow that terminates the runner process, starves it for CPU/Memory, or blocks its network access can cause this error.)).
Date
10 October 2026
Version
at the release’s recorded version
Their method
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
Re-run through Comparator did not reach a verdict (the job ended (failure) in the step "comparator, Lean’s kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.)).
Date
10 October 2026
Version
at the release’s recorded version
Their method
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
Re-run through Comparator did not reach a verdict (the job ended (failure) in the step "comparator, Lean’s kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.)).
Date
10 October 2026
Version
at the release’s recorded version
Their method
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator did not reach a verdict (the job ended (failure) in the step "comparator, Lean’s kernel and nanoda" without uploading a result: the runner terminated it (GitHub: Process completed with exit code 143.)).
Date
10 October 2026
Version
at the release’s recorded version
Their method
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.