Problem GT-001 — the Hadwiger–Nelson problem

Conjectura.Problems.GT001.Statement

/-
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
-/
import Conjectura.Defs.Mathematics.Combinatorics.GraphTheory.UnitDistanceGraph
import Mathlib.Analysis.InnerProductSpace.EuclideanDist
import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

/-! # Problem GT-001 — the Hadwiger–Nelson problem

LOCKED: solvers cannot modify this file.
-/

namespace Conjectura.GT001

/-- 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

end Conjectura.GT001