// four-color
FOUR COLOR
Re-verification of the Four Color Theorem's computer proofs, plus a new theorem.
// in plain terms
The Four Color Theorem says any map can be colored with four colors so no neighboring regions match. Its proof is famous for being checked by computer rather than by hand. We independently re-verified those decades-old computer proofs, found a bug in the canonical 1995 program, and extended a 110-year-old result in the process.
// 01
Prior verification
✓ valid — no two neighbors share a color
click a region to recolor it — try to break the theorem
Since 1976 the Four Color Theorem has been the emblem of computer-assisted proof. The checking programs themselves have been largely taken on faith: no one had independently re-derived them from the mathematics.
// 02
Method
We rebuilt the reducibility and discharging checkers from the published mathematics rather than porting existing code, verified every configuration exhaustively, and adjudicated disagreements with a third independent implementation and exact-rational certificates computed without a solver.
// 03
Findings
| proof | configurations | verdict |
|---|---|---|
| RSST 1995 | 633 | verified |
| Steinberger 2010 | 2,822 | verified |
| 2026 pool | 7,697 of 8,200 | verified — 430 shown removable |
- +The canonical 1995 reducibility oracle, reduce.c, miscomputes on 6 of 70 generic inputs (30–46% undercount). The behavior is fail-safe, but wrong.
- +A 12-row Farkas certificate settles an open discharging question over 5,895 configurations.
// 04
Result
New theorem: f(r) = 5, 5, 6, 7, 7, 8 for ring sizes 8–13, the minimum interior vertices for D-reducibility, exhaustive and triple-verified. It is the first quantitative extension of Birkhoff's 1913 bound.
// the thread
Status
Re-reading a proof the field had stopped reading turned up errors, compressions, and one new theorem. The extension of the old bound is small, but the bound had stood for 110 years. Next steps: finish the short paper for arXiv, file the reduce.c findings upstream, and Lean-check the certificate.
// papers
this page is the TL;DR — the papers are the full story. drafts, provided as-is.