Problem GT-001 — the Hadwiger–Nelson problem

goaldef

How many colours are needed so that no two points of the plane at distance one share a colour? De Grey showed in 2018 that five is not enough; seven suffice. Six remains undecided, which is what this asks.

def goal : Prop :=
  (Conjectura.GraphTheory.unitDistanceGraph (EuclideanSpace ℝ (Fin 2))).Colorable 6

Builds on

Unit-distance graph

From Mathlib

Analysis.InnerProductSpace.EuclideanDist
Combinatorics.SimpleGraph.Coloring.Vertex

import Conjectura.Problems.GT001.Statement · maintainer — open · raw source

Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors

Full credits