Erdős Problem #508
Hadwiger-Nelson problem

Read our full write-up →

Erdős asked for the chromatic number of the plane — the Hadwiger–Nelson problem — and the page's bounds were 5 ≤ χ ≤ 7, the five from de Grey's 2018 graph. OpenAI's 23 September 2026 paper proves that every five-colouring of the plane, with no regularity assumption on the colour classes, has two points at distance one of the same colour, so χ is 6 or 7. The proof transfers any colouring at all to a weak measurable one, for every number of colours (through a new rigidity theorem for rotation-invariant laws on the dual of the algebraic plane — false for the rational plane, which is exactly why Payne's two-colourable rational graph is no counterexample; the seats found the sentence that separates the two cases), and then excludes five weak-measurable labels by continua of common exclusion ending in a rational placement of the Moser spindle. Its catalogued Lean proof — 70 modules including the Furstenberg–Zimmer tower — compiled on our machine in 1,263 s with 0 errors; under --trust=0 #print axioms reported only propext, Classical.choice and Quot.sound for the theorem and, transitively, everything it rests on; the comparator's statement, copied verbatim, is proved by the solution's theorem; the page's lower-bound statement closes from it in three forms written from scratch; the six-colour and distance-2 controls fail. Seven tool-equipped seats, each briefed to refute, between them covered all 62 pages — each scoped seat line by line through its stretch — and found no gap — only exposition notes, an uncited 2014 precursor for the weak-measurable definition, and a theorem the paper leaves unstated: the measurable chromatic number of the plane is also at least 6, the first move past Falconer since 1981 if Theorem 1.4 holds. Five other parties record machine checks of the Lean; no human had refereed the paper. The exact value stays open. The theorem is OpenAI's; the audit, the replay and the statement probes are ours.