Hadwiger's conjecture
Hadwiger's conjecture asserts that every graph G satisfies χ(G) ≤ h(G), where h(G) is the largest order of a complete-graph minor of G. Three manuscripts dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) concern this conjecture and two related ones. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original results
- Counterexample to Hadwiger's conjecture. Arbitrarily large finite simple graphs with independence number at most two whose chromatic number exceeds their Hadwiger number; even their fractional chromatic number exceeds it, which also disproves the fractional weakening discussed by Reed and Seymour.
- Counterexample to the Colin de Verdière chromatic conjecture. Graphs with independence number at most two whose chromatic number, and even fractional chromatic number, exceeds their Colin de Verdière invariant by more than one.
- Linear list-coloring bound. There is an absolute integer C such that every finite nonempty graph satisfies χlist(G) ≤ C h(G), the Linear List Hadwiger conjecture.
- Sources (openai/math repository, commit
1581d4c): counterexample to Hadwiger's conjecture, Colin de Verdière chromatic conjecture, linear list-coloring bound. - Formalization, as described by the repository. The scope note lean/docs/157.md states that the formalization constructs arbitrarily large finite simple counterexamples with independence number at most two and proves h(G) < 26m/75 + 2/3 < m/2 ≤ χ(G) for a graph on m vertices, disproving the ordinary chromatic form; the fractional-chromatic strengthening and the Colin de Verdière consequence are outside that statement. It also states that the linear list-coloring bound is formalized.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 15 October 2026) |
|---|---|---|---|---|
| 2026-09-30 (last updated 2026-10-08) | jfairfaxball-348/Hadwiger-conjecture | Use (formalization) | A Lean 4 development built on the collection's formalization of the counterexample (ported to its toolchain), adding an independent Mathlib-only statement of the result and a Lean proof that the fractional weakening χf(G) ≤ h(G) is false. | The README reports that all its stated theorems compile with no sorry and depend only on the axioms propext, Classical.choice and Quot.sound.
|
| 2026-10-04 | Sergey Norin and Raphael Steiner, arXiv:2610.05291, A Proof of the Linear Hadwiger Conjecture | Parallel work | There is C such that every Kt-minor-free graph is Ct-colorable. The abstract states that the proof was found by GPT-6 Astra following the authors' directions. (The list-coloring bound claimed in the collection implies this chromatic form, since χ ≤ χlist.) | arXiv preprint, version 1. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.