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

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A linear list-coloring bound in terms of the Hadwiger number](../../preprints/A-linear-list-coloring-bound-in-terms-of-the-Hadwiger-number-September-23-2026/paper.pdf)
- [A counterexample to Hadwiger's conjecture](../../preprints/A-counterexample-to-Hadwigers-conjecture-September-23-2026/paper.pdf)

## 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](../ComparatorChallenges/ListHadwiger.lean) |
| Arbitrarily large counterexamples to Hadwiger's conjecture | [HadwigerCounterexample.lean](../ComparatorChallenges/HadwigerCounterexample.lean) |