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
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.
(SimpleGraph.UnitDistancePlaneGraph Set.univ).chromaticNumber ≤ 7TextbookStatement only, no proof