AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

A counterexample to Hadwiger's conjecture

Does the classical conjecture or property hold, or does there exist a counterexample as established in A counterexample to Hadwiger's conjecture?

Model / AI: OpenAI (unreleased)

machine-checked (counterexample)self-reported (counterexample)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 157)

Model / AI: OpenAI (unreleased)

machine-checked (counterexample)self-reported (counterexample)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'A counterexample to Hadwiger's conjecture'. 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.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 157). The Lean development was not rebuilt locally.