In October 1852, a young London-born mathematician named Francis Guthrie was colouring a map of the counties of England when he noticed something odd: four colours were enough to ensure that no two neighbouring counties shared a colour, and he could not construct any map that needed five. He mentioned it to his brother Frederick, then a student of the great logician Augustus De Morgan in London, and Frederick passed the question upstairs. De Morgan was hooked. That very day he wrote to his friend William Rowan Hamilton in Dublin, describing the problem and confessing he could not settle it. Hamilton, splendidly unbothered, replied that he was unlikely to attempt the question soon. He had a point, in a way nobody could have guessed: the question would swallow mathematicians whole for the next 124 years, and its eventual solution would ignite a philosophical row that has never entirely gone out.
The rules of the puzzle are stricter than they look. Regions count as neighbours only if they share a stretch of border — meeting at a single point, like the four corner states of the American West, does not count. Each region must also be a single connected patch, which is why real-world maps with exclaves, or requirements that overseas territories match their motherland, can genuinely demand five colours or more. Cartographers, it should be said, never much cared; real atlases use colour for all sorts of reasons and rarely aim for the minimum. The four colour problem was always pure mathematics wearing a cartographer's coat.
A proof that stood for eleven years
In 1878 Arthur Cayley revived the dormant problem at the London Mathematical Society, and the following year the barrister and amateur mathematician Alfred Kempe published a proof. It was elegant, widely admired, and wrong. The flaw hid for eleven years, until Percy Heawood exposed it in 1890. Heawood's demolition was constructive, though: salvaging what worked in Kempe's argument, he proved that five colours always suffice — leaving mathematics in the faintly comic position of knowing the answer was four or five, but not which, for most of a century. Kempe's ideas — his "chains" and his strategy of finding unavoidable configurations that could be reduced to smaller cases — remained the blueprint for everything that followed.
The endgame came at the University of Illinois. Kenneth Appel and Wolfgang Haken, assisted by John Koch and a then-remarkable allocation of computer time, pursued the Kempe strategy at industrial scale: show that every possible planar map must contain at least one configuration from a specific list, then show that each configuration on the list is "reducible" — that any map containing it can be shrunk to a smaller map in a way that preserves colourability, so no smallest counterexample can exist. Their list ran to 1,936 configurations (trimmed to 1,482 in the published version), and checking reducibility consumed roughly 1,200 hours of computer time in an era when that was a heroic quantity. In June 1976 they announced that four colours suffice. The university's mathematics department stamped its outgoing post with a new franking slogan: "Four colors suffice."
But is it a proof?
Then came the row. A traditional proof is something a competent mathematician can, in principle, read and verify from first premises to conclusion. No human being could read the Appel–Haken proof; the computer-checked portion was beyond any lifetime's verification by hand. In 1979 the philosopher Thomas Tymoczko published a much-cited paper arguing that the four colour theorem was therefore something new and troubling — a mathematical claim resting partly on empirical trust in machinery, more like a laboratory result than a deduction. Some mathematicians agreed, and grumbled that a proof no one could survey brought no understanding of why the theorem was true. Others retorted that human referees are hardly infallible — Kempe's flawed proof had passed eleven years of expert scrutiny, after all, which is not an argument computers should be embarrassed by.
The subsequent decades adjudicated the dispute in an unexpected way: the machines were vindicated by more machines. Nagging errors found in the original's hand-checked portions were repaired, and in 1996 Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas produced a cleaner computer-assisted proof needing only 633 configurations. Then, in 2005, Georges Gonthier of Microsoft Research formalised the entire theorem in the proof assistant Coq, so that every logical step — not just the case-checking — was verified mechanically down to the axioms. If you distrust that, you must distrust a tiny, heavily audited proof-checking kernel rather than thousands of pages of case analysis. Most mathematicians now sleep soundly; the philosophers, professionally, do not.
The four colour theorem thus carries a double legacy. It seeded whole tracts of graph theory, and it was the first major theorem whose proof was essentially a computation — the moment mathematics met the machine and had to decide what "knowing" means. A schoolboy's idle observation about English counties became the opening shot in an argument about the nature of proof itself. The maps were coloured long ago; what the colouring meant is still being argued over the atlas.
Quiz nuggets
- Francis Guthrie first conjectured in 1852, while colouring a map of English counties, that four colours suffice for any map.
- Alfred Kempe's 1879 proof of the four colour theorem stood for eleven years before Percy Heawood found the flaw in 1890 — and salvaged a proof that five colours suffice.
- Kenneth Appel and Wolfgang Haken proved the theorem at the University of Illinois in 1976, using about 1,200 hours of computer time to check 1,936 configurations.
- The University of Illinois marked the 1976 result with the postal franking slogan "Four colors suffice".
- Georges Gonthier fully formalised the four colour theorem in the Coq proof assistant in 2005, machine-verifying every logical step.