Concept
Any map can be colored with 4 colors — first major theorem proved by computer.
Understand it in one breath
Every planar map can be colored with only four colors so that adjacent regions differ. In 1976 Appel and Haken solved the 1852 problem by reducing the argument to finitely many cases and checking them by computer. It is widely described as the first major theorem proved with essential computer assistance, intensifying the question: "Is it a proof if no person can inspect every computation by hand?"
At a glance
Year | People | Advance |
|---|---|---|
1852 | Francis Guthrie | A question from his brother: noticed while coloring a map of Britain |
1879 | Kempe | Published a false proof that stood for 11 years |
1890 | Heawood | Found the flaw in Kempe’s proof and proved the Five Color Theorem |
1976 | Appel + Haken | Checked 1,936 cases by computer using 1,200 CPU hours |
1996 | Robertson et al. | Simplified the proof to 633 cases |
2005 | Gonthier | Formalized the proof in Coq for complete machine verification |
A landmark of computer-assisted proof — the first major theorem whose full computation was impractical to retrace by hand. Simpler proofs and formal verification followed.
Key formula
Key moments
A student’s question
London student Francis Guthrie was coloring a map of the counties of England when he conjectured that four colors would always suffice.
Kempe — a flawed proof
Arthur Kempe published a proof that was accepted for eleven years before a flaw was found in 1890.
Appel and Haken — a landmark computer-assisted proof
A computer checked 1,936 configurations, producing the first celebrated computer-assisted proof. Some mathematicians objected that a proof no person could inspect end to end was not really a proof.
Modern applications
Frequency assignment, timetable scheduling, compiler register allocation, GIS map coloring, and conflict avoidance.
Beyond MathVoyage
Loading…