Linear Hadwiger conjecture for graph colouring

Linear minor bound with Lean 4 formalization

Model / AI: GPT-6 Astra

Sergey Norin and Raphael Steiner prove the Linear Hadwiger Conjecture, showing that K_t-minor-free graphs are O(t)-colorable and settling the linear version of Hugo Hadwiger's 1943 conjecture. The authors state that the proof argument was found by GPT-6 Astra following human conceptual guidance, accompanied by a Lean 4 formal verification.

Source read 2026-10-08. Read the arXiv v1 preprint, proof outline, AI attribution disclosure, and linked Lean 4 project repository. The Lean code was not compiled locally.

• Paper — Paper
• Lean — Code and Lean repository