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:
Sources
FormalConjectures/ErdosProblems/
508.lean
Retained formal statement
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?
(SimpleGraph.UnitDistancePlaneGraph Set.univ).chromaticNumber = sorryOpenStatement only, no proof