Erdős problem 508
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:
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/508.lean4 ≤ (SimpleGraph.UnitDistancePlaneGraph Set.univ).chromaticNumberSolvedStatement only, no proof