The Euclidean plane is not five-colorable
The Euclidean plane is not five-colorable is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math). It concerns the Hadwiger–Nelson problem, which asks for the chromatic number χ(R2) of the plane: the least number of colors such that points at distance one always receive different colors. This page summarizes the published claim 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 result
- Claim. Every coloring of the Euclidean plane with five colors has a monochromatic pair of points at distance one, with no regularity assumption on the color classes. Together with Isbell's seven-coloring, this gives 6 ≤ χ(R2) ≤ 7.
- Method, as described in the paper's introduction. The proof has two parts: a transfer from unrestricted proper colorings to a measurable condition (a "weak measurable coloring"), which holds for every finite number of colors, and a geometric obstruction to five colors under that condition. The final step uses the two overlapping-triangle constraints of the Moser spindle. The proof does not exhibit a finite unit-distance graph that is not five-colorable; by the de Bruijn–Erdős compactness theorem such a graph exists if the theorem holds.
- Source. The Euclidean plane is not five-colorable in the openai/math repository (commit
adc7f12). - Formalization, as described by the repository. The scope note lean/docs/158.md states that the Lean formalization proves that five colors do not suffice, for arbitrary colorings with no measurability or continuity assumption, and that seven colors suffice, with every boundary point of the coloring regions included. The comparator statements are EuclideanFiveColor.lean and PlaneColoring.lean.
- Earlier published bounds. Nelson and Isbell (1950) gave the bounds 4 and 7. A. D. N. J. de Grey, The chromatic number of the plane is at least 5 (arXiv:1804.02385, 2018), gave the first finite unit-distance graph that is not four-colorable.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 14 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | Th1nhNg0/the-plane-needs-six (GitHub) | Exposition | An animated explainer video of the Hadwiger–Nelson problem, the Moser spindle and the preprint's proposed proof, with a discussion of what OpenAI reports about the AI's role and formal verification. | The README states that the video was created with Claude Opus 5.5 and ElevenLabs. |
| 2026-10-09 | Á. Dúcz, Measurable Independence Density Equals the Finite Independence-Ratio Infimum in the Euclidean Plane, Hexagon 2610.00171v1 | Use | V(G)| over finite unit-distance graphs G in the plane. Hence f(n)/n → m1(R2), where f(n) is the least independence number of a unit-distance graph on n vertices. The proof is nonquantitative. | Posted on Hexagon (v1), labelled "Primarily AI-generated text" with human understanding of "some parts". The provenance statement says that ChatGPT 6 was asked to produce the result with the techniques of OpenAI's paper and that, apart from this guidance, "the work was done entirely by ChatGPT". |
| 2026-10-09 (Lean rebuild); 2026-10-10 (forbidden distances) | S. Galán, decalion89/chromatic-number-of-the-plane (GitHub; Zenodo 10.5281/zenodo.22976635) | Extension; use | Rebuilds OpenAI's proof in Lean and runs it over the points constructible with ruler and compass, which therefore cannot be five-colored either (the step to every Euclidean field is on paper). States that OpenAI's transfer from arbitrary to measurable colorings also works for algebraic sets of forbidden distances and for fractional colorings, so that the fractional chromatic number of the plane is exactly 1/m1(R2), and gives certified lower bounds for several forbidden distances, such as χ(R2, {1, 2}) ≥ 7. The repository also places both bounds in the statement of Erdős Problem 508 from Google DeepMind's formal-conjectures project. | The README states that the code, computations and most of the text were produced with Claude under Sergi Galán's direction, and that "No result has been refereed or independently checked by a mathematician yet". |
| 2026-10-11 | S. Li, Y. Su, Every n points in the plane contain (m1 + o(1)) n points with no unit distance (arXiv:2610.15424, v1) | Use (formal) | If f(n) is the largest number such that every set of n points in the plane contains f(n) points with no two at distance 1, then f(n) = (m1 + o(1))n, where m1 is the supremum of the upper densities of measurable planar sets with no two points at distance 1. This is the first half of a conjecture of Dúcz and Varga; with the bound m1 ≤ 0.247 of Ambrus, Csiszárik, Matolcsi, Varga and Zsámboki it gives f(n) ≤ (0.247 + o(1))n. The abstract names the Haar rigidity theorem for wild character laws from OpenAI's preprint as the only non-classical input. | arXiv v1. The abstract states that the whole argument has been formalized in Lean 4 on top of OpenAI's formalization. |
| 2026-10-12 | punk01-shaka/hadwiger-nelson-audit (GitHub) | Verification (formal); critique of a check | Restates the theorem in a file importing only Mathlib and checks OpenAI's Lean proof against it in three ways: a full build with #print axioms, the Lean FRO's Comparator, and the independent kernel nanoda. In each case only the standard axioms propext, Quot.sound and Classical.choice are used. Separately reports that OpenAI's published Comparator configuration for this result accepts a fake three-line proof because of a "definition hole" (9 of 416 configurations, covering 8 results), and states that "This does not mean those results are wrong, only that the published automated check doesn't establish them." |
Audit report and red-team files are public in the repository. |
Related work
- J. Davies, Measurable obstructions for unmeasurable colourings (arXiv:2610.12301, v1, 8 October 2026), proves that the measurable and ordinary chromatic numbers of Rd agree for d ≥ 4, with further bounds, and names the extension to d = 2 as a possible route to the Hadwiger–Nelson problem. The acknowledgments state that the paper was posted earlier than planned because of OpenAI's release.
Notes
- Several follow-ups state substantial AI assistance, as recorded in the table.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.