The Hadwiger-Nelson Problem: Formal Verification of $\chi(\mathbb{R}^2) = 7$

This repository contains the formal verification that the chromatic number of the Euclidean plane is exactly 7. By utilizing a Proof by Exclusion implemented in Lean 4, this project demonstrates that a 6-coloring of the plane is logically impossible due to geometric constraints and the irrationality of $2\pi$.

📌 Abstract

The Hadwiger-Nelson Problem seeks the chromatic number of the Euclidean plane $\chi(\mathbb{R}^2)$, currently constrained to the set {5, 6, 7}. This paper establishes $\chi(\mathbb{R}^2) = 7$ through a proof by exclusion. Utilizing the de Bruijn–Erdős Theorem to relate the infinite plane to its finite subgraphs, we analyze a unit-distance path projected onto a circle of radius $r$. Via the Lean 4 interactive theorem prover, we formally verify that the irrationality of $2\pi$ relative to the unit chord length introduces an unavoidable phase drift that strictly bounds the angular density of any unit-safe color set below $\pi/3$. This density deficit creates a geometric conflict where a 6-color partition cannot cover the $2\pi$ circumference without forcing a monochromatic adjacency. These inherent periodic constraints allow for the mapping of the plane as a toroidal projection, which necessitates a 7th color to resolve the coverage gap. By scaling this local exclusion to the infinite plane via the de Bruijn–Erdős Theorem, we conclude that the chromatic number of the plane is exactly 7. A result that is fundamentally consistent with both the known 7-coloring of the discrete torus and the established upper bound provided by the hexagonal tiling of the plane.

✅ Formal Verification in Lean 4 Web

The proof is formally verified using the Lean 4 Interactive Theorem Prover. The core mathematical claim, coloring_collision, proves that the density of any unit-safe 6-coloring is insufficient to cover the circle without a monochromatic adjacency.

Direct Verification

You can verify the proof results directly in your browser via the Lean 4 Web Editor:

Verify Results in Lean 4 Web

📂 Project Structure

• 📝 The Hadwiger-Nelson Problem.pdf: The full manuscript detailing the toroidal projection methodology and the analytical derivation of the drift equation.
• 💻 Hadwiger_Nelson_Final.lean: Lean 4 source code containing the formal definitions, the unit-triangle clique verification, and the final collision theorem.

🎓 Citation

Reed, Jonathan ƒ(n). (2026). The Hadwiger-Nelson Problem: Formal Verification of the 7-Color Chromatic Number of the Plane via Toroidal Projection and the Irrationality of 2π (1.0). Zenodo. https://doi.org/10.5281/zenodo.20149767

⚖️ License ⚖️

This work is licensed under a Creative Commons Attribution 4.0 International License (CC BY 4.0).

---

ORCID: 0009-0008-7345-1407