The Unique Games Conjecture - Revision history

Aftermath bot: Add OpenAI's public reasoning summary (reasoning_traces) as a source

2026-10-15T06:32:19Z

Add OpenAI's public reasoning summary (reasoning_traces) as a source

← Older revision		Revision as of 23:32, 14 October 2026
Line 5:		Line 5:
	* '''Direct hardness results.''' Four further manuscripts give NP-hardness proofs that do not pass through the Unique Games Theorem and use established PCP and Label Cover hardness results: Max-Cut beyond the Goemans–Williamson ratio ([https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Direct-Proof-of-Optimal-Max-Cut-Hardness-September-23-2026 ''A direct proof of optimal Max-Cut hardness'']), Vertex Cover below factor two ([https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Factor-Two-Hardness-Threshold-for-Vertex-Cover-September-23-2026 ''The factor-two hardness threshold for Vertex Cover'']), and Min-UnCut and directed feedback vertex set within every fixed constant factor ([https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Constant-factor-hardness-of-Min-UnCut-September-23-2026 Min-UnCut], [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Constant-factor-hardness-of-directed-feedback-vertex-set-September-23-2026 directed feedback vertex set]).		* '''Direct hardness results.''' Four further manuscripts give NP-hardness proofs that do not pass through the Unique Games Theorem and use established PCP and Label Cover hardness results: Max-Cut beyond the Goemans–Williamson ratio ([https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Direct-Proof-of-Optimal-Max-Cut-Hardness-September-23-2026 ''A direct proof of optimal Max-Cut hardness'']), Vertex Cover below factor two ([https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Factor-Two-Hardness-Threshold-for-Vertex-Cover-September-23-2026 ''The factor-two hardness threshold for Vertex Cover'']), and Min-UnCut and directed feedback vertex set within every fixed constant factor ([https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Constant-factor-hardness-of-Min-UnCut-September-23-2026 Min-UnCut], [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Constant-factor-hardness-of-directed-feedback-vertex-set-September-23-2026 directed feedback vertex set]).
	* '''Consequences, as described in the manuscript.''' The Unique Games Theorem supplies the Unique Games hypothesis in earlier hardness reductions for cut, covering, constraint-satisfaction, ordering, deletion and clustering problems; the manuscript attributes those reductions and thresholds to their original authors (among them Khot, Kindler, Mossel and O'Donnell; Khot and Regev; Raghavendra).		* '''Consequences, as described in the manuscript.''' The Unique Games Theorem supplies the Unique Games hypothesis in earlier hardness reductions for cut, covering, constraint-satisfaction, ordering, deletion and clustering problems; the manuscript attributes those reductions and thresholds to their original authors (among them Khot, Kindler, Mossel and O'Donnell; Khot and Regev; Raghavendra).
			* '''Reasoning summary.''' The collection also contains an abridged summary of the model's reasoning for this family, ''Ordinary NP-hardness at the basic semidefinite threshold'' ([https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/reasoning_traces/basic-semidefinite-threshold-np-hardness.pdf reasoning_traces/basic-semidefinite-threshold-np-hardness.pdf], listed in the repository's [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/README.md README]). Its prompt asks for NP-hardness of beating the basic semidefinite-programming threshold of every fixed finite Max-CSP without assuming the Unique Games Conjecture. The summary presents a proposed argument in two stages: first Unique Games hardness with nearly perfect completeness and arbitrarily small soundness, starting from Håstad's hardness for nearly satisfiable parity equations and using projection-game parallel repetition and inverse-shortcode results; then a transfer to the basic-SDP threshold of each fixed constraint language through Raghavendra's dictatorship-test framework.
	* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/102.md lean/docs/102.md] states that the Lean formalization gives, for every fixed 0 < ε, δ < 1/2, a deterministic polynomial-time reduction from binary 3SAT to nonempty unweighted simple bipartite unique games with the stated completeness and soundness, over a fixed alphabet '''F'''<sub>2</sub><sup>''s''</sup> with translation constraints; it also formalizes the Max-Cut, Vertex Cover, Min-UnCut and directed feedback vertex set results.		* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/102.md lean/docs/102.md] states that the Lean formalization gives, for every fixed 0 < ε, δ < 1/2, a deterministic polynomial-time reduction from binary 3SAT to nonempty unweighted simple bipartite unique games with the stated completeness and soundness, over a fixed alphabet '''F'''<sub>2</sub><sup>''s''</sup> with translation constraints; it also formalizes the Max-Cut, Vertex Cover, Min-UnCut and directed feedback vertex set results.

Aftermath bot: Unique Games: Elbassioni-Gajjala-Ray geometric stabbing (arXiv 2607.28062 v2) uses the theorem

2026-10-15T01:47:57Z

Unique Games: Elbassioni-Gajjala-Ray geometric stabbing (arXiv 2607.28062 v2) uses the theorem

← Older revision		Revision as of 18:47, 14 October 2026
Line 9:		Line 9:
	== Public follow-up work ==		== Public follow-up work ==
	{\| class="wikitable"		{\| class="wikitable"
	! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)		! Date !! Work !! Relation !! Public claim !! Public status (checked 15 October 2026)
	\|-		\|-
	\| 2026-10-08 \|\| [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math at commit <code>adc7f12</code>, tables at repository commit <code>cd0063d</code>, 13 October 2026) \|\| Review (fidelity of the formal statements) \|\| An independent, pre-referee review of whether each Lean statement says what the paper claims. Its per-family table rates this family "full", and its per-challenge table records Comparator passes for the five challenges: run in a sandbox for Vertex Cover and Min-UnCut, without a sandbox for the Unique Games and optimal Max-Cut challenges, and not yet run for directed feedback vertex set. \|\| The review states that "full" means the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet.		\| 2026-10-08 \|\| [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math at commit <code>adc7f12</code>, tables at repository commit <code>cd0063d</code>, 13 October 2026) \|\| Review (fidelity of the formal statements) \|\| An independent, pre-referee review of whether each Lean statement says what the paper claims. Its per-family table rates this family "full", and its per-challenge table records Comparator passes for the five challenges: run in a sandbox for Vertex Cover and Min-UnCut, without a sandbox for the Unique Games and optimal Max-Cut challenges, and not yet run for directed feedback vertex set. \|\| The review states that "full" means the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet.
	\|-		\|-
	\| 2026-10-09 \|\| R. D. Barish, [https://github.com/RBarish-UTokyo/Max3SAT-MaxSNP-APX-Lean4 RBarish-UTokyo/Max3SAT-MaxSNP-APX-Lean4] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-09-000010&version=1 PALOMAR-2026-10-09-000010], version 1) \|\| Use (formal) \|\| A Lean 4 proof of the PCP theorem (gap and verifier forms) and of MaxSNP- and APX-completeness of MAX-3-SAT and 3-occurrence MAX-3-SAT for an explicit single-tape Turing machine model. The registry record states that it includes 194 files of OpenAI's Unique Games formalization, adapted to the Lean module system. \|\| Registered in the Palomar registry on 9 October 2026.		\| 2026-10-09 \|\| R. D. Barish, [https://github.com/RBarish-UTokyo/Max3SAT-MaxSNP-APX-Lean4 RBarish-UTokyo/Max3SAT-MaxSNP-APX-Lean4] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-09-000010&version=1 PALOMAR-2026-10-09-000010], version 1) \|\| Use (formal) \|\| A Lean 4 proof of the PCP theorem (gap and verifier forms) and of MaxSNP- and APX-completeness of MAX-3-SAT and 3-occurrence MAX-3-SAT for an explicit single-tape Turing machine model. The registry record states that it includes 194 files of OpenAI's Unique Games formalization, adapted to the Lean module system. \|\| Registered in the Palomar registry on 9 October 2026.
			\|-
			\| 2026-10-11 \|\| [https://arxiv.org/abs/2607.28062 arXiv:2607.28062] (v2), K. Elbassioni, R. Gajjala and S. Ray; titled ''Tight Approximation Thresholds for Geometric Stabbing'' \|\| Use \|\| Version 1 (30 July 2026) proved tight hardness thresholds for geometric stabbing problems under the Unique Games Conjecture, through a transfer theorem built on the strict-CSP framework of Kumar, Manokaran, Tulsiani and Vishnoi. Version 2 (11 October 2026) states the thresholds as NP-hardness results: for every ε > 0, square stabbing within 2 − ε, horizontal-segment stabbing within ''e''/(''e'' − 1) − ε, and, for every fixed ''d'' ≥ 2, cube stabbing and separated ''d''-interval transversal within ''d'' − ε. The text cites the Unique Games Theorem (Theorem 1.1) and a strong-left Unique Games source (Lemma A.1) of the OpenAI manuscript for the hardness input; the abstract does not mention it. \|\| arXiv v2.
	\|}		\|}

Aftermath bot: New page: The Unique Games Conjecture (openai/math 102) with MathVet review and Palomar-registered PCP formalization; Main Page link

2026-10-14T04:21:16Z

New page: The Unique Games Conjecture (openai/math 102) with MathVet review and Palomar-registered PCP formalization; Main Page link

New page

'''The Unique Games Conjecture''' is the subject of five manuscripts dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]). The conjecture, introduced by Khot in 2002, asserts that systems of permutation constraints can be hard to approximate even when almost all constraints can be satisfied; many optimal inapproximability thresholds had been proved assuming it. This page summarizes the published claims 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.

== The original results ==
* '''Claim (Unique Games Theorem).''' For every fixed ε, δ ∈ (0, 1/2) there are an integer ''s'' ≥ 1 and a deterministic polynomial-time reduction from 3SAT to explicit unweighted Unique Games instances over the alphabet ''K'' = '''F'''2''s'', on simple bipartite graphs with translation constraints, such that satisfiable formulas give value at least 1 − ε and unsatisfiable formulas give value at most δ. The manuscript states that this resolves the conjecture positively in its usual edge-value formulation. Source: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Unique-Games-Theorem-September-23-2026 ''The Unique Games Theorem''].
* '''Direct hardness results.''' Four further manuscripts give NP-hardness proofs that do not pass through the Unique Games Theorem and use established PCP and Label Cover hardness results: Max-Cut beyond the Goemans–Williamson ratio ([https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Direct-Proof-of-Optimal-Max-Cut-Hardness-September-23-2026 ''A direct proof of optimal Max-Cut hardness'']), Vertex Cover below factor two ([https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/The-Factor-Two-Hardness-Threshold-for-Vertex-Cover-September-23-2026 ''The factor-two hardness threshold for Vertex Cover'']), and Min-UnCut and directed feedback vertex set within every fixed constant factor ([https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Constant-factor-hardness-of-Min-UnCut-September-23-2026 Min-UnCut], [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Constant-factor-hardness-of-directed-feedback-vertex-set-September-23-2026 directed feedback vertex set]).
* '''Consequences, as described in the manuscript.''' The Unique Games Theorem supplies the Unique Games hypothesis in earlier hardness reductions for cut, covering, constraint-satisfaction, ordering, deletion and clustering problems; the manuscript attributes those reductions and thresholds to their original authors (among them Khot, Kindler, Mossel and O'Donnell; Khot and Regev; Raghavendra).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/102.md lean/docs/102.md] states that the Lean formalization gives, for every fixed 0 < ε, δ < 1/2, a deterministic polynomial-time reduction from binary 3SAT to nonempty unweighted simple bipartite unique games with the stated completeness and soundness, over a fixed alphabet '''F'''2''s'' with translation constraints; it also formalizes the Max-Cut, Vertex Cover, Min-UnCut and directed feedback vertex set results.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math at commit <code>adc7f12</code>, tables at repository commit <code>cd0063d</code>, 13 October 2026) || Review (fidelity of the formal statements) || An independent, pre-referee review of whether each Lean statement says what the paper claims. Its per-family table rates this family "full", and its per-challenge table records Comparator passes for the five challenges: run in a sandbox for Vertex Cover and Min-UnCut, without a sandbox for the Unique Games and optimal Max-Cut challenges, and not yet run for directed feedback vertex set. || The review states that "full" means the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet.
|-
| 2026-10-09 || R. D. Barish, [https://github.com/RBarish-UTokyo/Max3SAT-MaxSNP-APX-Lean4 RBarish-UTokyo/Max3SAT-MaxSNP-APX-Lean4] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-09-000010&version=1 PALOMAR-2026-10-09-000010], version 1) || Use (formal) || A Lean 4 proof of the PCP theorem (gap and verifier forms) and of MaxSNP- and APX-completeness of MAX-3-SAT and 3-occurrence MAX-3-SAT for an explicit single-tape Turing machine model. The registry record states that it includes 194 files of OpenAI's Unique Games formalization, adapted to the Lean module system. || Registered in the Palomar registry on 9 October 2026.
|}

== Notes ==
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]