The Hadwiger–Nelson problem

Reference: Wikipedia

At least 5 colors are required: de Grey 2018

theorem HadwigerNelson.HadwigerNelsonProblem : (SimpleGraph.UnitDistancePlaneGraph ⊤).chromaticNumber = sorry

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?

theorem HadwigerNelson.HadwigerNelsonAtLeastFive : 5 ≤ (SimpleGraph.UnitDistancePlaneGraph ⊤).chromaticNumber

It was established in 2018 that at least 5 colors are required for the Hadwiger-Nelson problem.

See reference: de Grey 2018

theorem HadwigerNelson.HadwigerNelsonAtMostSeven : (SimpleGraph.UnitDistancePlaneGraph ⊤).chromaticNumber ≤ 7

A simple construction that tiles the plane with hexagons can be used to show that 7 colors suffice for the Hadwiger-Nelson problem.