Theorem 3.1: $k$ -degenerate graphs are $(k+1)$ -colourable

Proved

HadwigerConj.colorable_of_isDegenerate

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

graph-coloringgraph-minorsgraph-theory

Let $G$ be a finite graph and $k\ge 0$ . If $G$ is $k$ -degenerate (every nonempty set $S$ of vertices contains a vertex with at most $k$ neighbours in $S$ ), then

\chi(G)\le k+1.

This converts bounds on degeneracy (for instance from average-degree bounds for graphs excluding a minor) into colouring bounds.

Preamble

import Mathlib
import Definitions.Def_HadwigerConj_Defs

Formal statement

namespace HadwigerConj
theorem colorable_of_isDegenerate {V : Type} [Finite V] (G : SimpleGraph V) (k : ℕ)
    (hG : IsDegenerate G k) : G.Colorable (k + 1) := by sorry
end HadwigerConj

Source

P. Seymour, "Hadwiger's conjecture" (survey), in: Open Problems in Mathematics, Springer, 2016 (uploaded PDF `paper.pdf`), Theorem 3.1 (p. 4)

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.

Let $V$ be a finite type, $G$ a simple graph on $V$ and $k\in\mathbb N$ . Suppose that for every nonempty $S\subseteq V$ there is $v\in S$ having at most $k$ neighbours inside $S$ . Then $G$ is properly colourable with $k+1$ colours.

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

Theorem 3.1: kkk-degenerate graphs are (k+1)(k+1)(k+1)-colourable

Theorem 3.1: $k$ -degenerate graphs are $(k+1)$ -colourable