Graph coloring, clique minors, and Colin de Verdière invariants

3 papersLean

Disproves Hadwiger's conjecture even for fractional coloring: arbitrarily large finite simple graphs with independence number at most two satisfy \(\chi_f(G)\gt h(G)\), where \(h(G)\) is the largest clique-minor order. Also disproves the fractional Colin de Verdière chromatic bound \(\chi_f(G)\le\mu(G)+1\). In the positive direction, every finite nonempty graph satisfies \(\chi_{\mathrm{list}}(G)\le C h(G)\) for a universal constant C.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 3

A counterexample to Hadwiger's conjecture

OpenAI · September 23, 2026

We disprove Hadwiger's conjecture by constructing arbitrarily large graphs whose chromatic number exceeds their Hadwiger number. The examples have independence number at most two, and even their ordinary fractional chromatic number exceeds their Hadwiger number. Thus they also disprove the fractional-coloring weakening discussed by Reed and Seymour.

Read PDF Download Source

Cite

@misc{OAI:A-counterexample-to-Hadwigers-conjecture-September-23-2026,
  author = {{OpenAI}},
  title = {{A counterexample to Hadwiger's conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-counterexample-to-Hadwigers-conjecture-September-23-2026/paper.pdf}{OAI:A-counterexample-to-Hadwigers-conjecture-September-23-2026}},
  year = {2026}
}

A counterexample to the Colin de Verdière chromatic conjecture

OpenAI · September 23, 2026

We disprove the Colin de Verdière chromatic conjecture by constructing graphs whose chromatic number exceeds their Colin de Verdière invariant by more than one. The examples have independence number at most two. In fact, their ordinary fractional chromatic number also exceeds their Colin de Verdière invariant by more than one.

Read PDF Download Source

Cite

@misc{OAI:A-counterexample-to-the-Colin-de-Verdiere-chromatic-conjecture-September-23-2026,
  author = {{OpenAI}},
  title = {{A counterexample to the Colin de Verdi{\`e}re chromatic conjecture}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-counterexample-to-the-Colin-de-Verdiere-chromatic-conjecture-September-23-2026/paper.pdf}{OAI:A-counterexample-to-the-Colin-de-Verdiere-chromatic-conjecture-September-23-2026}},
  year = {2026}
}

A linear list-coloring bound in terms of the Hadwiger number

OpenAI · September 23, 2026

We prove that every finite nonempty graph G satisfies \(\chi_{\mathrm{list}}(G)\le C h(G)\) for an absolute integer C, where \(h(G)\) is the largest order of a clique minor. This resolves the Linear List Hadwiger conjecture affirmatively.

Read PDF Download Source

Cite

@misc{OAI:A-linear-list-coloring-bound-in-terms-of-the-Hadwiger-number-September-23-2026,
  author = {{OpenAI}},
  title = {{A linear list-coloring bound in terms of the Hadwiger number}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-linear-list-coloring-bound-in-terms-of-the-Hadwiger-number-September-23-2026/paper.pdf}{OAI:A-linear-list-coloring-bound-in-terms-of-the-Hadwiger-number-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

Hadwiger's conjecture predicts \(\chi(G)\le h(G)\) for every finite graph, where \(h(G)\) is the largest clique-minor order. The formalization constructs arbitrarily large finite simple counterexamples with independence number at most two. For a graph on \(m\) vertices it proves \(h(G)<26m/75+2/3<m/2\le\chi(G)\). This disproves the ordinary chromatic form. The paper's fractional-chromatic strengthening and the Colin de Verdière consequence are outside this selected statement.

The Linear List Hadwiger conjecture asks for a universal linear bound on list chromatic number in terms of clique-minor size. The formalization proves that there is one integer \(C\ge1\) such that every finite nonempty simple graph \(G\) satisfies \(\chi_{\mathrm{list}}(G)\le C h(G)\), where \(h(G)\) is the largest order of a clique minor. The constant is independent of the graph.

Comparator links

Result	Comparator statement
Linear list-coloring bound in the Hadwiger number	ListHadwiger.lean
Arbitrarily large counterexamples to Hadwiger's conjecture	HadwigerCounterexample.lean

Scope note on GitHub →