we-solve (beta)

CS-172 · computer science · mathematics · Computational complexity · Graph theory and combinatorics

Factor-two hardness of Vertex Cover

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

For each fixed $0<\varepsilon\le1$, is it NP-hard, under deterministic polynomial-time reductions, to return a vertex cover of a finite simple unweighted graph whose size is at most $(2-\varepsilon)$ times the minimum? A vertex cover meets every edge. The graph is explicitly encoded; no degree bound or indistinguishability promise is imposed.

Short English statement

Is every fixed improvement of the factor-two approximation for Vertex Cover NP-hard on simple unweighted graphs?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

CS-172-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for CS-172

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.

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

Go to contribution →