Kostochka–Thomason: no $K_t$ minor $\Rightarrow$ $O(t\sqrt{\log t})$ -colourable

Proved

HadwigerConj.kostochka_thomason_colorable

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

graph-coloringgraph-minorsgraph-theory

There is an absolute constant $C$ such that for every $t\ge 1$ , every finite graph with no $K_t$ minor is colourable with $\lceil C\,t\sqrt{\log t}\,\rceil$ colours:

K_t\not\preceq G\ \Longrightarrow\ \chi(G)=O\big(t\sqrt{\log t}\big).

It follows from the Kostochka–Thomason bound on the average degree of graphs with no $K_t$ minor (Theorem 3.6 of the survey) via degeneracy; the survey notes this was long the best bound for large $t$ .

Formalization Note $\log$ is the natural logarithm; the colour count is the ceiling (as a natural number) of $C t\sqrt{\log t}$ .

Preamble

import Mathlib
import Definitions.Def_HadwigerConj_Defs

Formal statement

namespace HadwigerConj
theorem kostochka_thomason_colorable :
    ∃ C : ℝ, ∀ t : ℕ, 1 ≤ t → ∀ (V : Type) [Finite V] (G : SimpleGraph V),
      ¬ HasCompleteMinor G t → G.Colorable ⌈C * t * Real.sqrt (Real.log t)⌉₊ := by sorry
end HadwigerConj

Source

P. Seymour, "Hadwiger's conjecture" (survey), in: Open Problems in Mathematics, Springer, 2016 (uploaded PDF `paper.pdf`), Section 3, paragraph after Theorem 3.12 (p. 7: “every graph with no K_t minor has degeneracy at most O(t(log t)^{1/2}), and therefore chromatic number at most the same”); Wikipedia, "Hadwiger conjecture (graph theory)", https://en.wikipedia.org/wiki/Hadwiger_conjecture_(graph_theory), section “Special cases and partial results”

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Note — non-blind read-back. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the intended meaning. It is not independent or blind testimony, and no reviewer should treat it as such; an independent audit is still needed.

There exists a real number $C$ such that for every natural number $t\ge 1$ , every finite type $V$ and every simple graph $G$ on $V$ : if $G$ has no $K_t$ minor then $G$ is properly colourable with $\lceil C\cdot t\cdot\sqrt{\ln t}\,\rceil$ colours (the ceiling taken as a natural number, negative values giving $0$ ). At $t=1$ this number is $0$ , and a graph with no $K_1$ minor has no vertices. Here, for graphs $H$ on a vertex type $W$ and $G$ on a vertex type $V$ , “ $H$ is a minor of $G$ ” means: there are sets $B_w\subseteq V$ ( $w\in W$ ) such that (i) each $B_w$ induces a connected subgraph of $G$ (in particular $B_w\neq\emptyset$ ), (ii) $B_{w_1}\cap B_{w_2}=\emptyset$ whenever $w_1\neq w_2$ , and (iii) whenever $w_1w_2$ is an edge of $H$ , some vertex of $B_{w_1}$ is adjacent in $G$ to some vertex of $B_{w_2}$ . “ $G$ has a $K_t$ minor” means the complete graph on the $t$ -element set $\{0,\dots,t-1\}$ is a minor of $G$ in this sense (so: $t$ pairwise disjoint connected nonempty vertex sets, every two joined by an edge of $G$ ; for $t=0$ this holds for every graph). “ $k$ -colourable” means there is a map from $V$ to a $k$ -element set of colours giving adjacent vertices different colours (for $k=0$ this forces $V=\emptyset$ ). All graphs are simple (no loops, no multiple edges).

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Kostochka–Thomason: no KtK_tKt​ minor ⇒\Rightarrow⇒O(tlog⁡t)O(t\sqrt{\log t})O(tlogt​)-colourable

Kostochka–Thomason: no $K_t$ minor $\Rightarrow$ $O(t\sqrt{\log t})$ -colourable