What was already known
Exoo, Fisher and Ismailescu proved the five-colour lower bound for regular 8-, 10- and 12-gon norms and posed the wider polygon question. Gehér established an upper bound of six for the 14-gon case.
AI involvement
An earlier AI-assisted archive supplied the finite graph and LRAT certificate. OpenAI Codex developed the geometric Lean argument that turns it into a colouring obstruction in the 14-gon norm; a human selected and directed the work.
The project credits Codex with the geometric Lean bridge from an exact unit-distance graph and LRAT four-colouring refutation to the plane theorem. An earlier AI-assisted archive supplied the graph and certificate; a human chose the task and directed the work. The AI-led label assesses the credited bridge, with the earlier archive credited separately.
Importance
Resolves the 14-gon case of a stated polygon-colouring question; the exact chromatic number remains five or six.
Limitations
The contribution is this one polygon case, not the general regular-polygon conjecture. The finite graph and certificate came from an earlier AI-assisted archive; the disclosed Codex work supplied the geometric Lean bridge to an actual normed plane. External mathematical review remains pending.
Technical verification
The pinned repository reports a successful public Lean build and axiom audit of the completed plane theorem, with an LRAT check for the finite graph obstruction. This is a source-reported machine check; AIProofWatch did not rerun it.
Formal checking
The repository reports a successful public Lean build and axiom audit of the completed theorem; the final proof connects exact unit-distance graph edges and an LRAT four-colouring refutation to the plane statement.
- Checker
- Lean kernel, as reported by MathIsEvenEasier
- Scope
- Every proper unit-distance colouring of the plane whose unit ball is the regular 14-gon uses at least five colours.
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
Few is the default when evidence for a higher level is insufficient. The sources describe human direction and presentation review but do not document a named person explaining the central proof. Few is the default from this evidence gap, not a finding that people cannot understand it.
Correction and publication history
Primary theorem, prior baseline, AI attribution and documented proof scope reviewed for non-notifying local inclusion.
Read this published revision