The Euclidean plane is not five-colorable

Follow-up works

• Shisheng Li and Yong Su, Every n points in the plane contain (m1 + o(1)) n points with no unit distance (arXiv:2610.15424, 11 Oct 2026). Proves f(n)/n → m1(R^2), identifying the limiting worst-case finite independence ratio with the maximal measurable unit-distance-avoiding density; the abstract states that its "only non-classical input is the Haar rigidity theorem for wild character laws" from this preprint. [AI-generated per source]
• Ákos Dúcz (contributor), Measurable Independence Density Equals the Finite Independence-Ratio Infimum in the Euclidean Plane (hexagon:2610.00171v1, 9 Oct 2026). Claims that m1(R^2) equals the infimum of independence ratios of finite unit-distance graphs, using this paper's spectral rigidity theorem as a black box and following its weak-measurable reduction. [AI-generated per source]
• Henry Bass, euclidean-chromatic-transfer (GitHub repository with five preprints) (GitHub, Oct 2026). Extends this paper's transfer theorem to R^n, claiming among other things χ(R^3) ≥ 7 and lower bounds for planes with two forbidden distances, with a Lean 4 project reusing modules from openai/math (the README says some numerical density bounds enter as explicit hypotheses); the acknowledgements state that results, proofs and formalization were developed with help from Claude (Anthropic).

Comments and discussion

• Joshua Zelinsky, Bluesky post (Bluesky, 6 Oct 2026). Early reaction to this paper: "it doesn't look like the method is a direction that the prior lit used".
• JoshuaZ (Joshua Zelinsky) and Archimedes, comments on Are OpenAI's math results "creative" in an important way? (LessWrong, Oct 2026). Archimedes collects reactions to this paper; JoshuaZ (10 Oct) points to a 2014 paper of Bachoc, DeCorte, de Oliveira Filho and Vallentin as precedent for the "weakly measurable coloring" notion and names the transfer theorem (Theorem 1.3) as the new idea.
• Dmitry Rybin (@DmitryRybin1), post on X (7 Oct 2026). Two-post thread calling the equivalence of arbitrary and "weakly measurable" colorings unexpected and contrasting the proof's use of amenable groups, Pontryagin duality and Furstenberg–Zimmer towers with the single finite graph behind the earlier ≥ 5 bound.
• Gabriel Gaster (@gabegaster), post on X (9 Oct 2026). Remarks on the proof's combination of "Pontryagin duality, ergodic theory, and amenable groups" and asks whether six colors can be ruled out.
• Dr.山川｜Visual Math (@MathWithShan), post on X (17 Oct 2026). Contrasts de Grey's explicit 1581-vertex graph from 2018 with this paper's proof, which the post describes as "reportedly non-constructive", via the weakly measurable colorings step.

Formalization

• OpenAI math release, The Euclidean plane cannot be colored with five colors: Lean scope notes (mirrored on mathcommunity/oai-math-revised) (release Lean docs, 2026-10-06). The release's own Lean statement of no proper five-coloring (EuclideanFiveColor.lean) and of a proper seven-coloring including boundaries (PlaneColoring.lean), with links to both comparator statements. [AI-generated per source]
• google-deepmind/formal-conjectures, FormalConjectures/ErdosProblems/508.lean (formal-conjectures, accessed 2026-10-21). Marks HadwigerNelsonAtLeastSix as solved, citing this preprint and linking the release's Lean proof; the overall problem statement for χ(R^2) remains open there.
• Shisheng Li and Yong Su, Erdős Problem #1070: f(n) = (m₁ + o(1)) n (Lean 4 development accompanying arXiv:2610.15424, Oct 2026). Formalizes the follow-up density theorem on top of this paper's Lean development, using the release's wild_fourier theorem and a copied import closure, with documented axiom checks. [AI-generated per source]

Related prior literature mentioned by others

• Christine Bachoc, Evan DeCorte, Fernando Mário de Oliveira Filho, Frank Vallentin, Spectral bounds for the independence ratio and the chromatic number of an operator (Israel J. Math. 202 (2014), 227–254; arXiv:1301.1054). Zelinsky's LessWrong comment cites a 2014 paper by these authors as precedent for the paper's weakly measurable coloring notion.

Possibly relevant literature (found by the agent, not checked)

• James Davies, Measurable obstructions for unmeasurable colourings (arXiv:2610.12301, 8 Oct 2026). Proves transference theorems equating ordinary and measurable chromatic numbers of R^d for d = 4 and d ≥ 5 and names extending this to d = 2 as a target; compare with the planar transfer theorem (Theorem 1.3).
• Maxim Didin and Vsevolod Voronov, The chromatic number of Euclidean space with dense color classes (arXiv:2607.19946, 22 Jul 2026). Constructs proper colorings of R^n with every color class dense (12 colors for the plane); relevant to the paper's point that its lower bound assumes no regularity of the color classes.

News and blogs

• Adam Spencer, The Maths-alanche. (NerdNews, Oct 2026). The section "Five colours ain't enough" introduces the unit-distance coloring problem and explains the manuscript's claimed reduction to six or seven colors and its Lean formalization.