The Hadwiger-Nelson problem: the Euclidean plane is not five-colorable
Color every point of the plane so that any two points at distance exactly receive different colors, with no regularity imposed on the color classes. The Hadwiger-Nelson problem asks for the least number of colors for which this is possible. Isbell's hexagonal coloring gives , the Moser spindle gives , and de Grey (2018) gave a finite unit-distance graph that is not four-colorable, so . Falconer (1981) showed that five colors are needed if the classes must be measurable. Is the plane five-colorable, that is, can ?
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Euclidean Ramsey theory; chromatic number of the plane
- Posed by
- Edward Nelson (1950, unpublished, with John Isbell's upper bound seven); published by Hugo Hadwiger (Elemente der Mathematik, 1961)
- Year posed
- 1950
- Years open
- 76y
- Solved
- 2026-09-23
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 55 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Every coloring of with five colors, with arbitrary (possibly non-measurable) color classes, has two points at distance of the same color. With the classical seven-coloring this gives . The route is a transfer theorem showing that a proper -coloring exists if and only if a 'weak measurable' -coloring (monochromatic unit pairs of measure zero) exists, for every finite , followed by a geometric obstruction to weak measurable five-colorings. It does not decide between six and seven, and it does not give a finite non-five-colorable unit-distance graph (one exists by de Bruijn-Erdos compactness, but none is exhibited).
What the AI did
The release README says the results were produced by an unreleased internal OpenAI model with a fixed procedure, on average about three hours of ChatGPT Pro thinking compute per result, and that some outputs build on earlier model results. This result is not among the README's exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region). The manuscript is authored 'OpenAI' and names no human author. Single manuscript, dated September 23, 2026; the release's overview counts it as one family.
Verification
No independent mathematician has checked this yet. Checked here: Theorem 1.1 of the manuscript was read against the Hadwiger-Nelson problem as posed (arbitrary color classes, unit distance in the Euclidean plane). lean/formalization.yaml lists a main result for this paper: OAI.EuclideanFiveColor.no_proper_five_coloring in OAI/Geometry/PlaneColoring/Five.lean, with comparator ComparatorChallenges/EuclideanFiveColor. Its challenge statement was read: there is no function from the complex plane to Fin 5 giving distinct colors to every pair at norm distance exactly 1, with no measurability hypothesis. That is the headline claim, not a narrower one. Permitted axioms are propext, Quot.sound and Classical.choice. Not rebuilt here. The proof passes through a transfer theorem (a proper k-coloring exists iff a weak measurable k-coloring exists, in ZFC), which is the step a reader should look at first. The paper says six versus seven remains open, and notes that a May 2026 public manuscript announcing chi = 7 rests on a false density bound.