2026-09-17 · article Hadwiger–Nelson problemdiscrete geometrygraph colouring

The Hadwiger–Nelson problem — f(α), the largest unit-distance graph with independence number at most α: f(3) = 10, and f(4) is 14 or 15

Leanmachine-checked (Lean 4 + mathlib, standard axioms only, no sorryAx, no native_decide; theorem names given) paperproved, not yet machine-checked computationchecked on this machine, within the range stated; not a claim made to the outside knowna restatement, a known theorem, or a check of the literature

How many colours are needed to colour the points of the plane so that no two points at distance 1 get the same colour?
(This minimum is the chromatic number of the plane, χ(ℝ²) — the chromatic number of the infinite graph joining pairs of points at distance 1.)

Finite subgraphs — unit-distance graphs, finitely many points of the plane with edges between the pairs at distance 1 — give lower bounds on χ(ℝ²) (de Bruijn–Erdős). The upper bound 7 comes from a tiling by regular hexagons. The hard side is the lower bound: building finite graphs that are densely joined.

The fractional route has a ceiling. Since χ_f ≤ 4.36, this route cannot produce χ ≥ 5. It measures a different quantity from de Grey's 5, and that is best said up front.

Here a unit-distance graph is a simple graph G on n vertices together with a placement p : Fin n → ℝ² at distinct points such that only the endpoints of edges are at distance 1 (non-edges are unconstrained). In Lean: Realiz G p := (∀ i j, G.Adj i j → sq2 (p i) (p j) = 1) ∧ Function.Injective p and FGe n α := ∃ G, (∃ p, Realiz G p) ∧ G.indepNum ≤ α (meaning f(α) ≥ n).

f(α) gives χ_f ≥ f(α)/α. But as §02 says, finite graphs with independence ratio below 1/4 are known to exist, so the point of this quantity is not to push the ratio down but the exact value of f(α), and the smallest graphs that attain it.

Lower bound. The disjoint union of a Moser spindle and a triangle, Moser ⊔ K₃ (10 vertices, 14 edges), is a unit-distance graph with independence number 3. LeanShiori1183.fGe_10_3 : FGe 10 3. The coordinates live in Q(√3, √11, √33), and the three identities s3² = 3, s11² = 11, s3·s11 = s33 close every edge.

Upper bound. That no unit-distance graph on 11 vertices has independence number ≤ 3 is said in two steps.

1. Enumeration of candidates (computation on this machine): among graphs on 11 vertices with α ≤ 3, the isomorphism classes passing ω ≤ 3, K_2,3-freeness, a minimum-degree condition and the u(m) test (the maximum number of edges of a unit-distance graph on m points, OEIS A186705) number 117. computation
2. Non-realisability certificates (Lean): for each of the 117 classes, ∀ p : Fin 11 → ℝ × ℝ, ¬ Realiz E p. LeanShiori1178.hn11_no_realiz (cands_card = 117)

Hence f(3) = 10 — to be read as certificates in Lean, completeness of the enumeration by computation.

Lower bound 14. Moser ⊔ Moser (14 vertices, 22 edges), independence number 4. LeanShiori1183.fGe_14_4 : FGe 14 4. In general, from α(G₁ ⊔ G₂) = α(G₁) + α(G₂) and the disjoint union of realisations, f(2k) ≥ 7k and f(2k+1) ≥ 7k+3 follow in one stroke for all k. LeanShiori1192.hn_lower_family (indepNum_sum, fGe_add). A trivial lower bound; nothing new in it.

Upper bound 15. No unit-distance graph on 16 vertices has α ≤ 4.

1. Enumeration of candidates: take a vertex v₀ of degree 5, split into A = N(v₀) (5 vertices) and H = the 10 non-neighbours, and assemble. H ranges over the 10-vertex graphs with α ≤ 3 (666 classes) that have minimum degree ≥ 3 — 571 classes — of which the 296 that are not realisable in the plane are discarded first, leaving 275 to run. The assembled candidates number 2,100 classes (993 true isomorphism classes). computation
2. Non-realisability certificates: for all 2,100 classes, ∀ p : Fin 16 → ℝ × ℝ, ¬ Realiz E p. LeanShiori1185.hn16_no_realiz (cands16_card = 2100; 2,093 of them also in the stronger form hn16_no_edges, which does not even use injectivity). The 296 classes discarded by the H filter are also non-realisable in Lean: Shiori1189.hn10_no_realiz (candsH_card = 296); the same machinery drops a further 103: hn10_no_realiz2 (candsH2_card = 103)

Hence 14 ≤ f(4) ≤ 15. What is left outside Lean is only the combinatorial side — the completeness of the enumeration, the isomorphism tests per cell, and the derivation of minimum degree ≥ 3 for H. The geometric side (the proof that nothing is realisable) is in Lean for both the candidates and the H filter.

n = 15, α = 4 is open. Of 146 cells, 114 are complete with 0 survivors; the remaining cells are stuck where trilateration has two free steps (in a unit-distance graph a 4-cycle is a rhombus, so one constraint becomes dependent). If it closes, f(4) = 14; if it hits, a witness for f(4) = 15. computation f(5) ≤ 24 is also computation only.

The non-realisability proofs are trilateration. A point v at unit distance from two already-placed points x, y is confined to two points on the perpendicular bisector of xy (trilat_core: for u ⊥ d the position is linear in λ, and the square root disappears). Coordinates are held in 160-bit fixed-point interval arithmetic; if every branch contradicts, the candidate is not realisable. Vertices with a remaining degree of freedom are handled by a branch-and-bound with a free angle that bisects boxes; vertices with no freedom are solved as an equation by the parallelogram step p_v = p_x + p_y − p_u (two points at unit distance from both x and y are symmetric about the midpoint of xy). On the enumeration side, the 60° class lemma — each 60° class spans only 3α points — drops candidates early.

A Lean certificate is just the shape of the tree and two integers. Each branch hands over integer bounds on λ; the boxes themselves are computed by Lean (lam_box uses integer multiplication only). So the certificates are small and close by kernel evaluation (decide +kernel). For the 2,100 candidates at n = 16, certificates for the 993 representatives sufficed, the rest being mapped onto them by an explicit vertex map (close_relabel).

Where the open items that have moved now stand is collected in What remains. Only what is open at present is listed here.

Open at present

Sources and reproduction

Nothing in this article moves the known frame. The exact values f(3) = 10 and f(4) ∈ {14, 15} were not found in the literature searched, but they are the kind of value that may be obvious to a specialist. Novelty is claimed only as far as "not found in the literature searched".