Hadwiger's conjecture for t = 7: are K7-minor-free graphs 6-colourable?
Difficulty 73: t = 6 needed the Four Colour Theorem, and for t = 7 even 7-colourability has been open since Jakobsen's 8-colour bound of 1971; the 2025–26 two-edge-deleted cases show the density method advancing, but the full K7 case needs new structure. That places it above restriction in ℝ³ (72) and Erdős–Hajnal paths (69), below diagonal Ramsey (78). Application value 2.8: none. Leverage 39: the first open case of the central conjecture of graph colouring, just above Erdős–Hajnal paths (38).
The problem
If a network cannot be squeezed down to seven mutually linked dots, can it be coloured with six colours? Unknown.
- 1Colour a network so linked dots differ
- 2No K_t minor should need t-1 colours
- 3True up to 6; 5 equals Four Colour Theorem
- 4First open case: seven
Statement. Hadwiger's conjecture (1943) asserts that every graph with no minor is -colourable. A graph is a of if can be obtained from a subgraph of by contracting edges, and is the complete graph on vertices. It is known for : is equivalent to the by Wagner's theorem, and was reduced to the Four Colour Theorem by Robertson, Seymour and Thomas (1993). prove that every graph with no minor is -colourable. It is not even known whether -minor-free graphs are -colourable.
Path to understanding
foundations → problemThe research entries this problem rests on, in the order to read them. Each links to its explainer.
- Start with
- Step 2
- Step 3
- Graph minors and structural graph theoryTheory · host
- Then
- Hadwiger's conjecture for t = 7: are K7-minor-free graphs 6-colourable?The problem
State of the art
Jakobsen (1971) proved that K7-minor-free graphs are 8-colourable and that K7⁻-minor-free graphs (K7 minus an edge) are 7-colourable; these were re-proved by Albar and Gonçalves (arXiv:1304.5468; J. Graph Theory 2018) and Albar (arXiv:1402.2806). It is still not known whether K7-minor-free graphs are even 7-colourable, as Dvořák, Norin and Rahman state explicitly. Two recent preprints settle the target statement for K7 with two edges deleted: Norin and Totschnig (arXiv:2507.03244, July 2025) show every graph with no K7^∨ minor (two deleted edges sharing an endpoint) is 6-colourable, and Dvořák, Norin and Rahman (arXiv:2609.17760, September 2026) do the same for K7^= (two disjoint deleted edges), together with an edge bound of 4n−8 for 5-connected K7^=-minor-free graphs; both are unrefereed. For general t, Delcourt and Postle (arXiv:2108.01633) proved χ = O(t log log t) and reduced the linear bound to graphs on at most about t·(log t)^5 vertices; Liu and Luo (arXiv:2609.06867, September 2026, unrefereed) improved this to O(t log log log t). Unverified claim (general t only). Norin and Steiner (arXiv:2610.05291, 4 October 2026, unrefereed) claim the linear Hadwiger conjecture: an absolute constant C with χ(G) ≤ C·h(G) for every graph. The paper states that the proof was found by an OpenAI model (GPT-6 Astra) following the authors' directions, that the human authors wrote the exposition and take responsibility for correctness, and that a Lean 4 formalization of the full proof and its external inputs (Delcourt–Postle reduction, Reed–Seymour fractional bound) was produced with OpenAI Codex and is public. The argument combines a (4+ε)t bound for graphs of order at most t(log t)^{1/2−ε} with a bootstrap that raises the admissible order exponent, then invokes the Delcourt–Postle reduction. The authors estimate C ≈ 10^100, so even if correct the result says nothing about t = 7; no independent check of the paper or the Lean build was found as of 16 October 2026 (see the Verification board). The K7 case remains open.
Realistic applications
None practical. Hadwiger's conjecture is the central problem in structural graph colouring, and its methods (density of minor-free graphs, contraction-critical graphs) feed graph minor theory.
What counts as solved
A refereed proof that every K7-minor-free graph is 6-colourable, or a K7-minor-free graph with chromatic number at least 7.
How it gets verified
Expert reviewOnly expert review of the argument is possible today.
The statement is that every K7-minor-free graph is 6-colourable. Neither Mathlib nor Formal Conjectures (Formal Conjectures pinned at commit e754a78 (17 October 2026)) defines graph minors or states Hadwiger's conjecture, so the statement cannot be written without new definitions, and a proof is expected to be long and computer-assisted. A counterexample graph with chromatic number at least 7 could be verified by checking minor-freeness and non-6-colourability, which is hard but finite. Referees check any proof.
Claims under verification
+ add a claimWhere the work is
Needs new structural and density theorems for minor-free graphs; computation assists with discharging-style case checks.
Bottlenecks
ranked by votes- #1TheoryEdge density of K7-minor-free graphs is not sharp enough
Colouring proofs for small t use extremal edge-density bounds; for K7 the sharp bound for highly connected graphs is only established for variants with edges deleted (e.g. 4n−8 for K7^= in 5-connected graphs). The full K7 density structure is unresolved.
Community grades
Sign in to add your own grade.
Connected problems
Progress
- Oct 4, 2026Linear Hadwiger claimed (preprint, AI-assisted)source
Norin and Steiner claim χ ≤ C·h(G) with C ≈ 10^100, crediting GPT-6 Astra with the proof and releasing a Lean formalization. Unrefereed and not independently verified; no consequence for t = 7.
- Sep 15, 2026K7 minus two disjoint edges: 6-colourable (preprint)source
Dvořák, Norin and Rahman prove the K7^= case and a 4n−8 edge bound for 5-connected graphs.
- Sep 6, 2026O(t log log log t) (preprint)source
Liu and Luo improve the Delcourt–Postle bound to O(t log log log t) (v2 of their preprint, unrefereed).
- Jul 4, 2025K7 minus two adjacent edges: 6-colourable (preprint)source
Norin and Totschnig prove 6-colourability for K7^∨-minor-free graphs.
- Aug 3, 2021O(t log log t) and reduction to small graphs