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
historicReferences
History & 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.
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.