Four colour theorem

Solved, 1976Combinatorics and discrete mathematics

Statement

The regions of any planar map can be coloured with at most $4$ colours so that no two regions sharing a boundary curve (more than isolated points) receive the same colour. Equivalently, every loopless planar graph $G$ is $4$ -vertex-colourable, meaning its chromatic number satisfies $\chi(G) \le 4$ .

After Alfred Kempe's celebrated 1879 proof stood for eleven years before Percy Heawood exposed a flaw in 1890 (salvaging the $5$ -colour theorem), the problem became the first major theorem proved with essential computer assistance. In 1976, Kenneth Appel and Wolfgang Haken (with programming assistance from John Koch) combined Heesch's method of discharging with an exhaustive computer verification of $1{,}936$ (later reduced to $1{,}476$ ) reducible configurations, using over $1{,}200$ hours of IBM 370 machine time. Because a human referee could not hand-check the computer case analysis, the proof sparked philosophical debate. In 1997, Neil Robertson, Daniel P. Sanders, Paul Seymour, and Robin Thomas published a streamlined proof needing only $633$ configurations and a cleaner discharging rule. Finally, in 2005, Georges Gonthier (building on joint work with Benjamin Werner) completed a fully machine-checked formalisation of the Robertson–Sanders–Seymour–Thomas proof inside the Coq proof assistant, removing all doubt about software bugs or unverified case checks.

Solved by, 1976Kenneth Appel Solved by, 1976Wolfgang Haken

Ironically, map colouring on closed surfaces of higher Euler characteristic was settled before the planar case: Percy Heawood proved in 1890 that any map on a surface of Euler characteristic $\chi < 2$ requires at most $H(\chi) = \lfloor (7 + \sqrt{49 - 24\chi})/2 \rfloor$ colours (for example $7$ colours on the torus, where $\chi = 0$ ), and Gerhard Ringel and J. W. T. Youngs proved in 1968 that this bound is sharp for every surface except the Klein bottle (which needs $6$ rather than $7$ ). Stronger variants in the plane include Carsten Thomassen's 1994 theorem that every planar graph is $5$ -choosable (whereas $4$ -choosability fails), Herbert Grötzsch's 1959 theorem that every triangle-free planar graph is $3$ -colourable, and Hugo Hadwiger's still-open 1943 conjecture that every graph with no $K_t$ minor is $(t - 1)$ -colourable (whose case $t = 5$ is equivalent to the four colour theorem).

References

Kenneth Appel, Wolfgang Haken (1977). Every planar map is four colorable. Part I: Discharging · DOI:10.1215/ijm/1256049011
Neil Robertson, Daniel P. Sanders, Paul Seymour, Robin Thomas (1997). The Four-Colour Theorem · DOI:10.1006/jctb.1997.1750
Georges Gonthier (2008). Formal Proof—The Four-Color Theorem

History of the problem

1852While colouring a map of the counties of England, Francis Guthrie notices that $4$ colours suffice and asks his brother Frederick, a student of Augustus De Morgan; De Morgan immediately communicates the problem to William Rowan Hamilton.
1879Alfred Bray Kempe publishes a celebrated proof using alternating two-colour chains (Kempe chains); Peter Guthrie Tait publishes a second proof in 1880 reducing the theorem to $3$ -edge-colouring of $3$ -regular bridgeless planar graphs.
1890Percy John Heawood discovers a fatal flaw in Kempe's argument for degree- $5$ vertices when two Kempe chains intertwine, proves the $5$ -colour theorem using what remains valid, and generalises the map-colouring problem to surfaces of higher genus $g \ge 1$ .
1969Heinrich Heesch systematises the method of discharging and reducibility, showing how to reduce the problem to testing a finite unavoidable set of local configurations and pioneering computer algorithms for D-reducibility.
1976Kenneth Appel and Wolfgang Haken, assisted by John Koch, announce the first complete proof of the four colour theorem (published in 1977 in the Illinois Journal of Mathematics), using a computer to verify the reducibility of an unavoidable set of $1{,}936$ configurations.Kenneth Appel Wolfgang Haken
1997Neil Robertson, Daniel P. Sanders, Paul Seymour, and Robin Thomas publish a simplified proof with $32$ discharging rules and $633$ reducible configurations, whose computer check runs in hours rather than weeks.
2005Georges Gonthier completes a fully formalised, machine-checked proof of the four colour theorem inside the Coq proof assistant (published in the Notices of the AMS in 2008), verifying both the combinatorial hypermap theory and all $633$ reducibility computations.