Hadwiger’s conjecture disproved? (OpenAI, Lean)

Your AI and this story

Key facts

• Manuscript (abstract, verbatim): ‘We disprove Hadwiger’s conjecture by constructing arbitrarily large graphs whose chromatic number exceeds their Hadwiger number. The examples have independence number at most two, and even their ordinary fractional chromatic number exceeds their Hadwiger number. Thus they also disprove the fractional-coloring weakening discussed by Reed and Seymour.’ 104 pages, dated 23 Sept 2026
• Mechanism (paper, Theorem 1.1): arbitrarily large m-vertex graphs with α(G) ≤ 2 and connected matching number below m/100; a counting inequality gives h(G) ≤ (m + 4·cm(G) + 2)/3, while α(G) ≤ 2 forces χ_f(G) ≥ m/2. Corollary 1.2: h(G) < 26m/75 + 2/3 < m/2 ≤ χ_f(G) ≤ χ(G). By these bounds the chromatic number exceeds the Hadwiger number by a factor tending to 75/52 ≈ 1.44
• Background: Hadwiger conjectured in 1943 that every graph with no K_t minor is (t−1)-colourable; Bollobás, Catlin and Erdős called it ‘one of the deepest unsolved problems in graph theory’. It was known for t ≤ 6 (Robertson–Seymour–Thomas, 1993) and open for all larger t (Wikipedia). Its odd-minor strengthening was disproved by Kühn, Sauermann, Steiner and Wigderson (arXiv 2512.20392, Dec 2025), and the linear relaxation χ ≤ C·t was proved on 4 Oct 2026 by Norin and Steiner with a proof found by GPT-6 Astra (see Linear Hadwiger conjecture proved)
• Companions in family 157 (all dated 23 Sept): ‘A counterexample to the Colin de Verdière chromatic conjecture’ (131 pages; χ exceeds the Colin de Verdière invariant by more than one, again with α ≤ 2) and ‘A linear list-coloring bound in terms of the Hadwiger number’ (42 pages; ‘This resolves the Linear List Hadwiger conjecture affirmatively’). Gu and Xu (arXiv 2610.01946v2) say a key new ingredient of OpenAI’s list-colouring proof is a linear choice-number bound for small K_t-minor-free graphs, and give a shorter proof of a weaker form of it
• Lean: OpenAI’s initial 6 Oct release formalized only the list-colouring bound (ListHadwiger). The challenge HadwigerCounterexample was added in the 7 Oct update (commit 3014888, pushed 8 Oct 05:03 UTC); the scope note says it proves h(G) < 26m/75 + 2/3 < m/2 ≤ χ(G) for arbitrarily large graphs with α ≤ 2, which ‘disproves the ordinary chromatic form’, with the fractional and Colin de Verdière statements ‘outside this selected statement’. Both challenges were ‘accepted’ in the oai-math-revised comparator run of 25–26 Oct
• Independent formal work: a Lean repository by the GitHub account EdouardBonnet vendors the release’s construction and also derives the fractional consequence h(G) < 26m/75 + 2/3 < m/2 ≤ χ_f(G) ≤ χ(G); its README reports a complete local kernel replay on 11 Oct (Lax archive submission lax-342547)
• No explicit witness: Carlos Toledo’s audit lists the Hadwiger graphs among 15 headline objects that are ‘random or sufficiently large constructions given only by a prescription’, adding: ‘Where the Lean is kernel-checked (Hadwiger, Sidorenko, Ryser) the existence is formally proved; the gap is that nobody can look at the object.’ An AI-assisted survey (Ying Xie, arXiv 2610.17090) rates the method as new and notes the argument gives no explicit graph
• Reactions: Gil Kalai (7 Oct): ‘The new announcement gives counterexamples to the original conjecture, even among graphs with independence number at most two.’ Wikipedia now says ‘In October 2026, a bulk release by OpenAI included a claimed disproof of the conjecture.’ No assessment by a structural graph theorist found (web, Hacker News, oai-math-revised notes) as of 29 Oct