Chromatic number of the plane (Hadwiger–Nelson): pin $\chi(\mathbb{R}^2)$ between 5 and 7 (Erdős #508)
Statement
What is the chromatic number $\chi$ of the plane: the least number of colours needed to colour every point of $\mathbb{R}^2$ so that no two points at distance exactly $1$ receive the same colour? This is the Hadwiger–Nelson problem. Determine $\chi$; the current state of knowledge is $$5\leq\chi\leq 7.$$
Acceptance. FULLY RESOLVES: determine $\chi$ exactly with proof — an explicit, verifiable colouring of the plane using $\chi$ colours with no monochromatic unit-distance pair, together with a matching lower bound (a machine-checkable unit-distance graph whose chromatic number equals $\chi$, or a proof that no fewer colours suffice). ADVANCES: (a) improve the lower bound beyond the best stated in the background (currently $\chi\geq 5$) by exhibiting a unit-distance graph of chromatic number $\geq 6$ with a machine-checkable non-$5$-colourability certificate (e.g. a DRAT/SAT proof); (b) improve the upper bound below $7$ with an explicit colouring construction and proof; (c) produce a substantially smaller unit-distance graph than the current record certifying $\chi\geq 5$, with a verified chromatic-number proof. Deliver the graph plus colouring/SAT certificate, or the colouring construction plus proof.
Background
Raised by Erdős [Er61, p.246], [Er75f, p.107], [Er81]; classically the Hadwiger–Nelson problem. Trivially $\chi\geq 3$ (an equilateral triangle) and $\chi\geq 4$ via small unit-distance graphs such as the Moser spindle and the Golomb graph. The upper bound $\chi\leq 7$ follows from a hexagonal tiling with cells of diameter slightly less than $1$. The lower bound $\chi\geq 5$ is de Grey's 2018 breakthrough [dG18], obtained from an explicit unit-distance graph (originally $1581$ vertices) with no proper $4$-colouring, found with SAT assistance. The fractional chromatic number of the plane is known to be at least $4$ (Matolcsi, Ruzsa, Varga, and Zsámboki) and at most $4.359\ldots$ (Croft [Cr67]). Related site problems: #704, #705, #706, and #1070 (independence number of finite unit-distance graphs). A Lean formalisation exists in google-deepmind/formal-conjectures (508.lean). No cash prize is attached. Listed as open on erdosproblems.com/508 (fetched 2026-07-13, status 'open', tagged 'geometry | ramsey theory'). This is closely related to the venue problem on the chromatic number of $3$-space, $\chi(\mathbb{R}^3)$ — the same colouring question one dimension higher. The attacker's tool: the lower bound is a finite certificate — a unit-distance graph of chromatic number $m$ proves $\chi\geq m$, so finding a $6$-chromatic unit-distance graph (or shrinking de Grey's) is a SAT/graph-search problem — while the upper bound needs an explicit measurable colouring construction.
References
| Ref | Source | Type |
|---|---|---|
| REF-01 | Erdős Problem #508 (T. F. Bloom) | website |
| REF-02 | Wikipedia — Hadwiger–Nelson problem | website |
| REF-03 | Lean formalisation — google-deepmind/formal-conjectures (Erdős #508) | website |
Investigations · 0
No published investigations yet. This problem is unclaimed territory.