Science · Mathematics

The four colour theorem

1852–1976

Mathematics — graph theory and topology

The statement that any map drawn on a plane can be coloured with just four colours so that no two regions sharing a border have the same colour. Francis Guthrie noticed it in 1852 while colouring a map of the English counties, and his brother put it to Augustus De Morgan, who wrote to Hamilton about it on 23 October 1852. Alfred Kempe's 1879 "proof" stood for eleven years before Percy Heawood found the flaw, salvaging a five colour theorem from the wreckage. Kenneth Appel and Wolfgang Haken finally proved it at the University of Illinois in 1976, using some 1,200 hours of computer time — the first major theorem whose proof could not be checked by hand.

How to spot them

▸Four colours suffice for any map in the plane, with no two neighbours alike
▸Noticed in 1852 by a student colouring the counties of England
▸Kempe's 1879 proof survived eleven years before Heawood demolished it
▸Proved in 1976 by computer, causing a philosophical row about what a proof is
▸The Illinois department franked its post 'Four colors suffice'

Key facts

A student colouring the counties of England in 1852, and his brother's question to De Morgan (1852)

Francis Guthrie's observation; De Morgan wrote to Hamilton on 23 October 1852

Kempe's 1879 argument by chains, which stood unchallenged for eleven years (1879)

Alfred Bray Kempe's flawed proof; Kempe chains survive as a technique

Heawood's 1890 demolition, which rescued a weaker result with one colour to spare (1890)

Percy John Heawood found the flaw and proved that five colours always suffice

A 1976 Illinois result needing 1,200 hours of computer time and 1,936 configurations (1976)

Kenneth Appel and Wolfgang Haken — the first major theorem proved by computer

A celebratory postmark franked on University of Illinois mail from 1976 (1976)

It read 'Four colors suffice'

Georges Gonthier's 2005 verification in the Coq proof assistant (2005)

A fully machine-checked formal proof, answering doubts about the 1976 computation

On a doughnut's surface, seven colours are needed rather than four

The Heawood conjecture for the torus — a favourite follow-up question

Key ideas

Reduce the map to a graph: a vertex per region, an edge between neighbours. The claim becomes that every planar graph can be properly coloured with four colours.
The proof works by finding an unavoidable set of configurations, each of which is reducible — if a minimal counterexample existed it would have to contain one, and each can be four-coloured. Checking 1,936 configurations is what needed the computer.
The theorem holds for maps in which every country is a single connected region. Real atlases, with exclaves like Alaska or Kaliningrad, are not covered.

Quick-fire facts

•Francis Guthrie posed the question in 1852 while a student at University College London; his brother Frederick asked their teacher Augustus De Morgan
•De Morgan wrote to William Rowan Hamilton about it on 23 October 1852
•Alfred Bray Kempe published a proof in 1879 and was elected a Fellow of the Royal Society partly on the strength of it
•Percy John Heawood found the error in 1890 but salvaged the five colour theorem
•Heinrich Heesch developed the method of discharging in the 1960s, the key to the eventual proof
•Kenneth Appel and Wolfgang Haken completed the proof at the University of Illinois at Urbana-Champaign in June 1976
•Their proof checked 1,936 reducible configurations and used about 1,200 hours of computer time
•A simplified proof by Robertson, Sanders, Seymour and Thomas followed in 1996, still computer-assisted
•Georges Gonthier produced a fully formal, machine-verified proof in the Coq proof assistant in 2005
•On a torus, seven colours are needed; the general formula for surfaces is the Heawood number
•The proof provoked a lasting debate about whether a proof no human can read is really a proof

Drill it — 8 cards

1 / 8new card

Sources

MacTutor History of Mathematics Archive, University of St Andrews — The four colour theorem
Robin Wilson — Four Colors Suffice: How the Map Problem Was Solved