The Hadwiger–Nelson problem

Reference: Wikipedia

At least 5 colors are required: de Grey 2018

def HadwigerNelson.UnitDistancePlaneGraph : SimpleGraph (EuclideanSpace ℝ (Fin 2))

The unit-distance graph in the plane, i.e. the graph whose vertices are points in the plane and whose edges connect points that are exactly 1 unit apart.

Equations

• One or more equations did not get rendered due to their size.

theorem HadwigerNelson.HadwigerNelsonProblem : 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 ≤ 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 : 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.