Skip to content

Erdős problem 508

Start work

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:

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

508.lean

Retained formal statement1 of 5

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.

FormalConjectures/ErdosProblems/508.leanErdos508.HadwigerNelsonAtLeast41 lineExact file
4 ≤ (SimpleGraph.UnitDistancePlaneGraph Set.univ).chromaticNumber
SolvedStatement only, no proof