At least five colours for the regular fourteen-gon Minkowski plane

Let $C$ be a centrally symmetric convex curve and let $\chi(\mathbb R^2,C)$ be the least number of colours needed to colour the plane so that no two points at $C$ -norm distance one share a colour. Exoo, Fisher and Ismailescu proved $\chi(\mathbb R^2,C)\ge5$ for the regular octagon, decagon and dodecagon and asked (Problem 5.1) whether $\chi(\mathbb R^2,C)\ge5$ for every regular $2n$ -gon with $n\ge4$ . This entry is the case $n=7$ : with $P_{14}=\operatorname{conv}\{z\in\mathbb C:z^{14}=1\}$ as the unit ball, is $\chi(\mathbb R^2,P_{14})\ge5$ ?

Result: Proved(see note)
Status: Partial result
AI contribution: AI-discovered
Method: Computation
Field: Discrete geometry; unit-distance graph colouring
Posed by: Geoffrey Exoo, David Fisher and Dan Ismailescu, The chromatic number of the Minkowski plane: the regular polygon case, Problem 5.1 (arXiv:2108.12861, 2021)
Year posed: 2021
Years open: 5y
Solved: 2026-10-06
Model: OpenAI Codex (GPT-6 Astra)
Vendor: OpenAI
Collaborators: —
Verification: Lean-checked, statement unaudited
Publication: Announced
Significance: 8 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

We prove $\chi(\mathbb R^2,P_{14})\ge5$ using a graph with 1,540 vertices and 13,755 unit edges. Every edge difference is a rotated point on a side of the unit polygon with an exact algebraic parameter in $[0,1]$ . A kernel-checked LRAT refutation of the graph's four-colouring CNF rules out every four-colouring, and restricting a colouring of the plane to these points gives the contradiction. The whole geometric and logical chain is in Lean. With Gehér's upper bound, $5\le\chi(\mathbb R^2,P_{14})\le6$ ; whether five colours suffice remains open, as does Problem 5.1 for other $n$ .

What the AI did

An earlier AI-assisted research archive supplied the explicit graph, coordinates, CNF/LRAT certificate and finite logical bridge. OpenAI Codex (GPT-6 Astra) developed the complete geometric Lean proof, connected the obstruction to an actual normed real plane, removed the importer's unsafe term-evaluation calls, rebuilt the finite certificate and audited the final theorem. It also prepared the mathematical exposition and interactive diagrams. The human collaborator selected the result, directed the work, required full geometric formalization and reviewed the presentation. No independent human mathematical audit is claimed.

Verification

Checked by this site on 7 October 2026, not rebuilt here. No independent mathematician has checked this yet. The headline theorem at_least_five_colours (formal/Final.lean) was read: any colouring of the plane by n colours that separates every pair at distance one has n at least 5. Plane is the complex numbers as a real vector space with the gauge of the convex hull of the 14th roots of unity as norm, and its distance is that norm of the difference, so the formal statement matches the posed question. The project has no sorry, admit, axiom declarations or native_decide; its SAT importer adds its LRAT steps through addDecl, so the kernel checks them. The public Actions run 37468510724 (commit e0f5e2a, success, on the author's own self-hosted Azure runner) prints propext, Classical.choice and Quot.sound for the final theorem and the graph lemma; the formal sources have not changed since that commit. A separate check written here from the graph file: all 13,755 edges have 14-gon norm 1 to within 1e-15 in floating point, and a fresh four-colouring encoding solved by CaDiCaL is unsatisfiable (157 s). Gehér's upper bound six is cited, not formalised.

Sources

Submitted by ZestyRaven517 on 06 Oct 2026

At least five colours for the regular fourteen-gon Minkowski plane

What was actually shown

What the AI did

Verification

Sources

Discussion