The problem
Every planar graph is vertex-colourable with four colours: equivalently, every map of countries can be coloured with four colours so adjacent countries differ.
The Four Colour Theorem
historicHistory & significance
Guthrie's 1852 question, passed through De Morgan. Kempe's celebrated 1879 proof stood for eleven years until Heawood found the fatal flaw — and salvaged from it the five-colour theorem. Franklin, Birkhoff, and generations reduced the configurations needing analysis. Appel and Haken's 1976 computer proof settled it but left unease about hand-checked reducibility; Gonthier and Werner removed the last doubt in 2005 with a complete Coq formalization.
Connected problems
- related Hadwiger's Conjecture
- related The Robbins conjecture
- related The strong perfect graph theorem
References
- primaryRead the primary source →
The resolution (computer-assisted proof)
Proved by Kenneth Appel and Wolfgang Haken (with John Koch), 1976: an unavoidable set of 1,936 reducible configurations, discharged by roughly 1,200 hours of IBM 370-168 computation. Philosophers and mathematicians argued for decades about whether a proof no human can read in a lifetime deserves the name. The debate now reads as prophecy: half a century later, machines do not merely check our case analyses — they find the arguments.
Verified by curator — see the API for full claim provenance.