[`SimpleGraph`] Hadwiger-Nelson problem

[SnirBroshi]

Wikipedia
Numberphile

/-- https://en.wikipedia.org/wiki/Unit_distance_graph -/
def unitDistGraph (X : Type*) [MetricSpace X] : SimpleGraph X where
  Adj u v := Dist.dist u v = 1
  symm u v h := by simpa [_root_.dist_comm]

abbrev planeUnitDistGraph := unitDistGraph <| EuclideanSpace ℝ <| Fin 2

-- TODO: tile the plane with hexagons, color the hexagonal grid with 7 colors
def coloringPlaneUnitDistGraphSeven : planeUnitDistGraph.Coloring (Fin 7) := sorry

theorem five_le_chromaticNumber_planeUnitDistGraph : 5 ≤ planeUnitDistGraph.chromaticNumber := sorry

The Wikipedia page contains interesting results about higher dimensions.