OpenAI claim summary for CS-172
computer sciencemathematicsTop Open Problemscontributionliterature_reportClaim: literature report
Summary of a claim published in openai/math; not a claim by this platform.
The explicit gap theorem uses deterministic polynomial-time reductions to simple unweighted graphs. Its approximation corollary covers every fixed $1\le\alpha<2$, equivalently every $0<\varepsilon\le1$ with $\alpha=2-\varepsilon$. This matches the complete question with the corrected factor range.
Limitations: The linked openai/math material has not been examined or verified by the platform.
Manuscript
Contents
Factor-two hardness of Vertex Cover
OpenAI's claim
OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 102; 2026-09-23), the asserted result is that every fixed approximation factor strictly below two for Vertex Cover is NP-hard on simple unweighted graphs.Mathematical statement of the claimed result
Manuscript 1.
For every fixed factor $1\le\alpha<2$, the manuscript claims NP-hardness of approximating minimum Vertex Cover within factor $\alpha$. In particular, \[ (\exists\text{ deterministic polynomial-time }(2-\varepsilon)\text{-approximation}) \Rightarrow\mathrm P=\mathrm{NP}\quad\text{for every fixed }\varepsilon\in(0,1]. \] The optimum is minimum number of selected vertices meeting every edge in the unweighted graph.Outline of the argument
For manuscript 1 (family 102; 2026-09-23), compatible local-answer tables become graph vertices, with edges encoding failed consistency. An unusually large independent set gives conditional gradients and bounded label lists; pair decoding contradicts the source gap, while satisfiable inputs provide the matching independent-set density.Formal verification
For manuscript 1 (family 102; 2026-09-23), OpenAI lists Lean statements for this assertion: every fixed approximation factor strictly below two for Vertex Cover is NP-hard on simple unweighted graphs.The selected statement includes the clause used for this problem.
The linked family Comparator checks are DirectedFeedback.lean, MinUncut.lean, OptimalMaxCut.lean, UniqueGamesTheorem.lean, VertexCover.lean.
Their named declarations include OAI.DirectedFeedback.main, OAI.MinUncut.main, OAI.OptimalMaxCut.main, OAI.UniqueGamesTheorem.theorem11, OAI.VertexCover.every_fixed_factor_below_two, OAI.VertexCover.explicit_cover_gap.
This site has not executed the Lean code. Described statement coverage is not an independent proof check.
Status caveat
The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.Sources
- OpenAI, The Factor-Two Hardness Threshold for Vertex Cover, 2026-09-23; citation key
OAI:The-Factor-Two-Hardness-Threshold-for-Vertex-Cover-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:hardness; Statement source: thm:gap. - Family 102: Lean scope.
- Comparator DirectedFeedback.json.
- Comparator DirectedFeedback.lean.
- Comparator MinUncut.json.
- Comparator MinUncut.lean.
- Comparator OptimalMaxCut.json.
- Comparator OptimalMaxCut.lean.
- Comparator UniqueGamesTheorem.json.
- Comparator UniqueGamesTheorem.lean.
- Comparator VertexCover.json.
- Comparator VertexCover.lean.
- Family 102: Reasoning summary.
- OpenAI catalogue entry.