Documentation

FormalConjectures.ErdosProblems.«508»

Erdős Problem 508 #

Reference: erdosproblems.com/508

proven by considering the [Moser-Spindel graph] or the [Golomb graph] At least 4 colors are required: Moser-Spindel graph At least 4 colors are required: Golomb graph At least 5 colors are required: de Grey 2018

source
def Erdos508.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.
Instances For
    source
    def Erdos508.«termχ(ℝ²)» :
    Lean.ParserDescr
    Equations
    Instances For
      source
      theorem Erdos508.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?

      source
      theorem Erdos508.HadwigerNelsonAtLeastFive :
      5 ≤ UnitDistancePlaneGraph.chromaticNumber

      Aubrey de Grey improved the lower bound for the chromatic number of the plane to 5 in 2018 using a graph that has >1000 nodes.

      "The chromatic number of the plane is at least 5" Aubrey D. N. J. de Grey, 2018 (https://doi.org/10.48550/arXiv.1804.02385)

      source
      theorem Erdos508.HadwigerNelsonAtLeast4 :
      4 ≤ UnitDistancePlaneGraph.chromaticNumber

      The "chromatic number of the plane" is at least 4. This can be proven by considering the Moser-Spindel graph or the Golomb graph graph.

      source
      theorem Erdos508.HadwigerNelsonAtMostSeven :
      UnitDistancePlaneGraph.chromaticNumber ≤ 7

      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.

      source
      theorem Erdos508.HadwigerNelsonAtLeastThree :
      3 ≤ UnitDistancePlaneGraph.chromaticNumber

      The chromatic number of the plane is at least 3.

      This is proven by considering an equilateral triangle in the plane.