The Euclidean plane cannot be colored with five colors

1 paperLean

Proves that every five-coloring of the Euclidean plane has a monochromatic pair at distance one, with no restriction on the color classes. This advances the Hadwiger–Nelson problem: together with the classical seven-coloring, only six and seven remain possible chromatic numbers of the plane.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

The Euclidean plane is not five-colorable

OpenAI · September 23, 2026

We prove that every coloring of the Euclidean plane with five colors has a monochromatic unit-distance pair, with no regularity assumption on the color classes. Consequently, the chromatic number of the plane is either six or seven.

Read PDF Download Source

Cite

@misc{OAI:The-Euclidean-plane-is-not-five-colorable-September-23-2026,
  author = {{OpenAI}},
  title = {{The Euclidean plane is not five-colorable}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-Euclidean-plane-is-not-five-colorable-September-23-2026/paper.pdf}{OAI:The-Euclidean-plane-is-not-five-colorable-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

The Euclidean plane is not five-colorable

Scope

The Hadwiger–Nelson problem asks for the fewest colors needed to color the plane so that points at distance one have different colors. The formalized results prove that five colors do not suffice and that seven colors do suffice. The lower bound applies to arbitrary colorings, with no measurability or continuity assumption; the upper bound includes every boundary point of the coloring regions.

Comparator links

Result	Comparator statement
No proper five-coloring	EuclideanFiveColor.lean
Proper seven-coloring	PlaneColoring.lean

Scope note on GitHub →