Chromatic number of the plane

Upper bound, last-listed row

| $7$ | [Had1945], [CR2017] | A periodic $7$-coloring obtained from a tiling of the plane by small regular hexagons (historically attributed to Isbell, 1950). |tracked since 2026-07-24 — no movement seen yet

Lower bound, last-listed row

| $5$ | [deG2018] | First proof that $\chi(\mathbb R^{2})\ge 5$, via an explicit finite unit-distance graph. |tracked since 2026-07-24 — no movement seen yet

Outside the source table: a claim in OpenAI's math release

• Family 158, “The Euclidean plane cannot be colored with five colors”, claims that the plane cannot be coloured with five colours so that every two points at distance one get different colours.

  Its Lean statement, EuclideanFiveColor.lean:

  theorem no_proper_five_coloring : ¬ ∃ coloring : ℂ → Fin 5, ProperColoring 5 coloring

  Same quantity: the file takes the plane as the complex numbers with the usual distance, so the statement says this constant is at least 6, above the 5 in its last-listed lower-bound row. The same family's other Lean file, a 7-colouring, is the long-known upper bound.

  Status: a Lean statement of it is published with a proof by its authors. We read the statement and it matches this constant's definition; we have not compiled the proof, and we have not read the paper.

A claim in a preprint release, read at openai/math@fd4aeeb on 2026-10-12. It is not in the source table, and this ledger has not changed the rows above because of it.