Oct 6, 2026
Lean formalization in OpenAI math repository (Result 158)
Model / AI: OpenAI (unreleased)
machine-checked (formal proof)self-reported (formal proof)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'The Euclidean plane is not five-colorable'. 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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 158). The Lean development was not rebuilt locally.