# The Euclidean plane cannot be colored with five colors

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

- [The Euclidean plane is not five-colorable](../../preprints/The-Euclidean-plane-is-not-five-colorable-September-23-2026/paper.pdf)

## 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](../ComparatorChallenges/EuclideanFiveColor.lean) |
| Proper seven-coloring | [PlaneColoring.lean](../ComparatorChallenges/PlaneColoring.lean) |