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. (Lean)
Manuscript
The Euclidean plane is not five-colorable
September 23, 2026 · source · Lean formalization available · cite as \cite{OAI:The-Euclidean-plane-is-not-five-colorable-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.
Result 158 · Combinatorics. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Agora members.
Source: https://github.com/openai/math/blob/main/CONTENTS.md