Linear Hadwiger conjecture proved: K_t-minor-free graphs are O(t)-colourable; proof found by GPT-6 Astra (Norin & Steiner), Lean-verified by Codex
On Oct 4, 2026 Sergey Norin (McGill) and Raphael Steiner (ETH Zurich) posted arXiv 2610.05291, proving the linear Hadwiger conjecture: there is a constant C such that every graph with no K_t minor is Ct-colourable. The authors say the proof "was found by GPT-6 Astra, following the directions by the authors", and that almost none of their own proof ideas survived. A Lean 4 formalization of the main theorem, produced by OpenAI Codex (6 Sol and Astra), builds with no sorries.
Key facts
- Paper: 'A Proof of the Linear Hadwiger Conjecture', Sergey Norin and Raphael Steiner, arXiv 2610.05291 (math.CO), Oct 4, 2026
- Result: ∃ C ∈ ℕ such that K_t-minor-free graphs are Ct-colourable (Hadwiger's 1943 conjecture asks for t−1 colours; the linear version had been a major open weakening; best prior general bound was O(t log log t), Delcourt–Postle)
- Disclosure: 'The proof presented in this paper was developed by OpenAI's ChatGPT model Astra 6, following research directions and feedback supplied by the authors. The authors suggested several possible approaches, but almost none of their specific proof ideas were retained in the final argument.'
- Process: asked first for the very dense case (v(G) ≤ C′t), which the model proved 'after only a couple of hours and some encouragement'; then an explicit dependence gave the conjecture for v(G) ≤ t(log t)^(1/2−o(1)); asked for 'an original idea to bridge the gap', it produced the bootstrap argument that closes it using Delcourt–Postle's reduction
- Ingredients: Reed–Seymour fractional linear Hadwiger, Delcourt–Postle reduction and chromatic separability, Pippenger–Frankl–Rödl matching theorem, LP duality, Liu–Luo-style contractions; the authors: the proof is 'contained in the convex hull of existing results. Yet it does not lie on a low-dimensional face of it'
- Lean 4: github.com/snorin239/LinearHadwiger formalizes Theorem 1 (plus Reed–Seymour, Theorem 4, Corollary 24), produced by 'OpenAI Codex versions 6 Sol and Astra, following guidance from the paper's authors'; no sorries, standard axioms only; release v0.1.0
- Verification status: preprint + Lean-verified main theorem; not yet peer-reviewed
Science result
- Field
- mathematics / graph theory / graph colouring
- Problem
- Linear Hadwiger conjecture (K_t-minor-free graphs have chromatic number O(t)) (open since 1943)
- Result
- Proved: a universal C with χ(G) ≤ Ct for all K_t-minor-free G
- AI system
- GPT-6 Astra, OpenAI Codex (6 Sol, Astra)
- Human role
- AI-generated proof under human direction: authors set the strategy and sub-goals; GPT-6 Astra wrote essentially all of the proof; Codex produced the Lean formalization
- Verification
- Preprint; main theorem formally verified in Lean 4 (no sorries)
- Status
- pending
- Why surprising
- A central graph-colouring conjecture, the subject of decades of incremental bounds, was settled with a proof the human experts say they did not write.
What happened
Hadwiger's conjecture (1943) links graph minors and colouring; even its "linear" weakening, that O(t) colours suffice, resisted work by Reed, Seymour, Norin, Postle, Delcourt and others, whose best bounds were slightly superlinear. Norin, one of the field's main contributors, and Steiner directed GPT-6 Astra toward what they saw as the missing dense case. The model solved it quickly and, when pushed for a new idea, found a bootstrap argument that finishes the proof. Codex then formalized the main theorem in Lean.
Why it matters
With the 3SUM/APSP refutation and the KLS proofs posted the same week, it marks a step change in AI-originated mathematics: famous problems now fall with proofs largely written by models and checked by machines. Original Hadwiger (t−1 colours) remains open. Reactions had not been found at 07:30 CEST on Oct 6.
Changelog
- 2026-10-06: created (arXiv scan of the Oct 5 listing; disclosure quoted from the PDF)
People
Related events
- OpenAI releases GPT-6 Astra, its first GPT-6 model ★★★★★
- Summer 2026 flood: dozens of named conjectures settled on arXiv with disclosed AI help (July–September catalogue) ★★★★
- Claude discovers an algorithm that refutes the 3SUM and APSP hypotheses: truly subquadratic 3SUM and truly subcubic APSP (Alman & Vassilevska Williams, Lean-verified) ★★★★★
- Kannan–Lovász–Simonovits (KLS) conjecture proved in two AI-assisted preprints: Song–Zhang's O(1) bound, then Bizeul–Klartag–Lehec ('most proofs … found by ChatGPT') ★★★★★
Sources (2)
- paperarXiv 2610.05291: A Proof of the Linear Hadwiger Conjecture
- codeGitHub: snorin239/LinearHadwiger (Lean 4 formalization)
id: 2026-10-04-linear-hadwiger-conjecture-proved-gpt-6-astra · updated 2026-10-06 · open in the interactive timeline