508.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 4 contain sorry, 0 declared as axioms

Erdős Problem 508

Reference: erdosproblems.com/508

proven by considering the [Moser-Spindel graph] or the [Golomb graph] At least 4 colors are required: Moser-Spindel graph At least 4 colors are required: Golomb graph At least 5 colors are required: de Grey 2018

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Wikipedia/HadwigerNelson.lean

theorem Erdos508.HadwigerNelsonProblem The Hadwiger–Nelson problem asks: How many colors are required to color the plane such that no two points at distance 1 from each other have the same color? sorry line 46 source
Source documentation
The Hadwiger–Nelson problem asks: How many colors are required to color the plane such that no two points at distance 1 from each other have the same color?

depends on sorry what this means
Statement uses: Eq, ENat, SimpleGraph.chromaticNumber, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Set.univ, SimpleGraph.UnitDistancePlaneGraph, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem HadwigerNelsonProblem :
    χ(ℝ²) = answer(sorry) := by
…
```
theorem Erdos508.HadwigerNelsonAtLeastFive Aubrey de Grey improved the lower bound for the chromatic number of the plane to 5 in 2018 using a graph that has >1000 nodes sorry line 58 source
Source documentation
Aubrey de Grey improved the lower bound for the chromatic number of the plane to 5 in 2018 using a graph that has >1000 nodes.
"The chromatic number of the plane is at least 5" Aubrey D. N. J. de Grey, 2018 (https://doi.org/10.48550/arXiv.1804.02385)

depends on sorry what this means
Statement uses: LE.le, ENat, OfNat.ofNat, Nat, SimpleGraph.chromaticNumber, EuclideanSpace, Real, Fin, Set.univ, SimpleGraph.UnitDistancePlaneGraph
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem HadwigerNelsonAtLeastFive :
    5 ≤ χ(ℝ²) := by
…
```
theorem Erdos508.HadwigerNelsonAtLeast4 The "chromatic number of the plane" is at least 4 sorry line 68 source
Source documentation
The "chromatic number of the plane" is at least 4. This can be proven by considering the Moser-Spindel graph or the Golomb graph graph.

L4DEL explanation
The "chromatic number of the plane" is at least 4. This can be proven by considering the Moser-Spindel graph or the Golomb graph graph.
Sources and attribution: Pinned Lean source (1646ca16afd6)

depends on sorry what this means
Statement uses: LE.le, ENat, OfNat.ofNat, Nat, SimpleGraph.chromaticNumber, EuclideanSpace, Real, Fin, Set.univ, SimpleGraph.UnitDistancePlaneGraph
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem HadwigerNelsonAtLeast4 : 4 ≤ χ(ℝ²) := by
…
```
theorem Erdos508.HadwigerNelsonAtMostSeven This upper bound for the chromatic number of the plane was observed by John R sorry line 82 source
Source documentation
This upper bound for the chromatic number of the plane was observed by John R. Isbell. His approach was dividing the plane into hexagons of uniform size and coloring them with a repeating pattern. A proof can probably be found in:
Soifer, Alexander (2008), The Mathematical Coloring Book: Mathematics of Coloring and the Colorful Life of its Creators, New York: Springer, ISBN 978-0-387-74640-1
An alternative approach that uses square tiling was highlighted by László Székely.

depends on sorry what this means
Statement uses: LE.le, ENat, SimpleGraph.chromaticNumber, EuclideanSpace, Real, Fin, OfNat.ofNat, Nat, Set.univ, SimpleGraph.UnitDistancePlaneGraph
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem HadwigerNelsonAtMostSeven :
    χ(ℝ²) ≤ 7 := by
…
```
theorem Erdos508.HadwigerNelsonAtLeastThree The chromatic number of the plane is at least 3 line 90 source
Source documentation
The chromatic number of the plane is at least 3.
This is proven by considering an equilateral triangle in the plane.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: LE.le, ENat, OfNat.ofNat, Nat, SimpleGraph.chromaticNumber, EuclideanSpace, Real, Fin, Set.univ, SimpleGraph.UnitDistancePlaneGraph
Proof uses: SimpleGraph.le_chromaticNumber_of_pairwise_adj, Nat.succ, of_eq_true, Nat.card, Eq.trans, True, congrArg, Fintype.card, zero_add, Nat.card_eq_fintype_card, Fintype.card_fin, Matrix.vecCons, Subtype.mk, Membership.mem, Set, WithLp.toLp, ENNReal, Matrix.vecEmpty, Set.mem_univ, OfScientific.ofScientific and 87 more
147 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem HadwigerNelsonAtLeastThree : 3 ≤ χ(ℝ²) :=
…
```