Any map drawn on a flat plane can be coloured using only four colours so that no two regions sharing a border have the same colour. First conjectured in 1852, proved in 1976 by Kenneth Appel and Wolfgang Haken — the first major mathematical theorem whose proof required extensive computer verification, sparking philosophical debate about what counts as a mathematical proof.
Grab a map of any country divided into states or provinces. Try colouring each region so that no two regions sharing a border have the same colour (regions meeting only at a single point are allowed to match). How many colours do you need? The surprising answer: for any map, no matter how complicated, you never need more than four.
It's easy to check that four colours work for any specific map you try. The hard part is proving it works for every possible map that could ever be drawn — including maps far more complicated than anyone has actually drawn, with wildly irregular region shapes. That requires a mathematical argument covering literally all cases.
In 1976, Kenneth Appel and Wolfgang Haken finally proved the theorem — but their proof required a computer to check 1,936 special map configurations, a task that would have taken a human many years to do by hand. This was the first time in history that a major mathematical theorem's proof depended on a computer performing calculations no human could feasibly verify by hand — and it sparked genuine philosophical debate: is a proof that no human can fully check still a valid mathematical proof?
Any map can be converted into a graph: each region becomes a "vertex" (dot), and two vertices are connected by an "edge" (line) if their regions share a border. The map-colouring problem becomes: can every planar graph (one that can be drawn without edges crossing) have its vertices coloured with 4 colours so that no two connected vertices share a colour?
Some maps genuinely require 4 colours — for example, four mutually-bordering regions (like four countries all touching each other) force 4 distinct colours. But no map requires a fifth. The theorem says 4 is both necessary (for some maps) and sufficient (for all maps).
Alfred Kempe published a proof in 1879 that was accepted for 11 years, until Percy Heawood (1890) found a flaw in Kempe's argument. Kempe's technique — "Kempe chains," involving swapping colours along paths in the graph — turned out to be salvageable and was eventually incorporated into the successful 1976 proof, but his original argument had a genuine gap that took over a decade to notice.
A related, much easier result — that 5 colours always suffice — was proven rigorously by Heawood in 1890 using Kempe's repaired techniques. Going from 5 colours (provably easy) to 4 colours (extraordinarily hard) turned out to require an entirely different order of mathematical effort.
Appel and Haken's approach: show that every possible planar graph must contain at least one of 1,936 specific "unavoidable" local configurations, and then show that each of these 1,936 configurations can be individually resolved (reduced to a simpler case using Kempe-chain-style arguments). Both steps — establishing unavoidability and checking reducibility for all 1,936 cases — required massive computer calculation, totaling over 1,000 hours of computer time in 1976 (an enormous amount by the computing standards of that era).
The 1976 proof provoked significant debate in the philosophy of mathematics. Traditionally, a mathematical proof is something any sufficiently trained human can, in principle, check line by line. The Four Colour Theorem's proof involved checking 1,936 cases by computer — a task no human could realistically verify by hand in a lifetime. Critics (including philosopher of mathematics Thomas Tymoczko, 1979) argued this changed the fundamental nature of mathematical proof, introducing an unavoidable element of trust in computer hardware and software correctness that traditional proofs did not require. Others argued that computer verification is simply an extension of ordinary mathematical rigour, since traditional proofs also rely on trusting prior established results without personally re-deriving them from first principles.
In 2005, Georges Gonthier produced a formally verified proof of the Four Colour Theorem using the Coq proof assistant — a system that mechanically checks every logical step against formal axioms, providing a much higher standard of certainty than the original 1976 computer calculations (which, while extensive, were ordinary computer programs subject to potential undetected bugs, not formally verified against logical axioms). This 2005 verification substantially addressed the philosophical concerns about the reliability of the original proof.
Robertson, Sanders, Seymour, and Thomas (1997) produced a simplified proof reducing the number of unavoidable configurations from 1,936 to 633, and streamlining the reducibility verification — making the computer-assisted portion of the proof considerably more manageable, though still requiring substantial computation.
The theorem is specific to planar graphs (or equivalently, maps on a sphere). For maps drawn on more complex surfaces, more colours may be needed: the Heawood conjecture (proven by Ringel and Youngs, 1968, except for the case of the Klein bottle) gives a formula for the maximum number of colours needed on a surface of any given genus (number of "holes," like a torus/donut shape). For a torus, for example, 7 colours can be required — a map exists requiring all 7, and 7 always suffices.