MathIsEvenEasier / 14

Discrete geometry · A complete Lean proof

Four colours
are not enough.

Change the unit circle to a regular fourteen-gon. Colour every point of the plane so that points one unit apart have different colours.

You need at least five colours.

The lower bound is formalized, including the geometry. Whether five colours suffice for the whole plane remains open.

01 / What counts as one unit?

A whole side is at distance one.

Every point on the boundary has polygon norm 1. Its usual Euclidean length can vary.

The side lemma

Join two consecutive vertices of the polygon. Every point on this segment lies on its boundary: a supporting line keeps the whole polygon on one side.

p = ζj((1 − t) + tζ)
ζ = exp(πi/7),   0 ≤ t ≤ 1
Polygon norm of r·p1.00
Euclidean length0.975

Lean: rotated_side_unit ↗

02 / From a side to 13,755 edges

Inspect an actual edge of the obstruction.

The vertices below are the points in the certificate. Each listed edge comes with an exact side and an exact algebraic parameter.

Loading the certified graph…
The selected edge is highlighted; nearby incident edges provide context.

Exact witness

Loading…

Here ρ = 2 cos(2π/7). Lean proves 0 ≤ t ≤ 1 using exact rational bounds on this specific algebraic root.

See the integer coordinates
Each row (a₀,…,a₅) means a₀ + a₁ζ + ⋯ + a₅ζ⁵.
Open this witness in Lean ↗


The drawing uses floating-point approximations for display. The proof checks the integer identities and algebraic bounds exactly. It does not rely on pixels or numerical tolerances.


What does an edge forbid?
Try the same colour at both ends.
For each edge and colour c, the formula contains
¬x(u,c) ∨ ¬x(v,c). Equal colours violate this clause.
Vertex u
Vertex v


The full certificate proves that no assignment satisfies all the constraints together. This two-vertex interaction illustrates one constraint; it is not a search for a colouring of the full graph.






03 / Why the conclusion follows
Two branches meet in the plane.
The geometry proves these are unit edges. The finite certificate proves four colours cannot separate them. Select a node to see its role and formal source.






Read the formal source ↗


This map groups the main logical stages. It is not an exhaustive import graph of the 162 checked modules, and its boxes are not manuscript theorem numbers.


The last step has no finite-to-infinite leap.
Suppose the whole plane had a proper four-colouring c. Give graph vertex v the colour c(point(v)). Every graph edge has distance 1, so this would properly four-colour the finite graph. The certificate rules that out.
We only need the listed edges to have length 1. We do not need to list every unit pair or assume that all nonadjacent vertices map to different points.






04 / Check the claim
From the statement to the evidence.


1,540graph vertices
13,755certified edges
65,801colouring clauses
162checked modules


Exactly what Lean proves
theorem at_least_five_colours
    (c : Plane → Fin n)
    (proper : ∀ x y, dist x y = 1 → c x ≠ c y) :
    5 ≤ n
Lean 4.34.0 with a pinned mathlib revision. The complete theorem includes the normed real plane, the polygon unit ball, the edge geometry and the finite contradiction.
The final axiom dependencies are propext, Classical.choice and Quot.sound. Project proofs contain no custom axioms, sorry, unsafe or native_decide.
Three intentionally invalid controls were rejected. Independent expert review is pending.


Where this fits
Exoo, Fisher and Ismailescu established lower bounds of five for the regular 8-, 10- and 12-gon norms [2021]. Gehér gave an upper bound of six for even regular polygons with at most 22 vertices [2023].
The present lower bound and that published upper bound give 5 ≤ χ(ℝ², P₁₄) ≤ 6. The upper bound is cited, not included in this Lean development. We make no priority claim.