Proving four colours suffice for any map took 124 years and a computer
In October 1852 Francis Guthrie, colouring a map of English counties, noticed he never needed more than four colours to keep neighbouring counties distinct. His question baffled Augustus De Morgan. It was finally settled in 1976, by the first major proof that leaned heavily on a computer.
The rule sounds simple: shade any map so that regions sharing a stretch of border differ in colour, and four shades are always enough. Touching at a single point does not count, otherwise a pie cut into many slices would need endless colours. Nor does it cover countries with detached pieces, like Alaska or Russia's Kaliningrad; forcing both parts to match can demand a fifth colour. In graph terms, every network that can be drawn flat without crossing lines can have its points coloured with four colours so no linked pair match.
False dawns were plentiful. Alfred Kempe published a celebrated proof in 1879 and Peter Guthrie Tait another in 1880, and each stood unchallenged for 11 years before Percy Heawood and Julius Petersen found the holes. Heawood salvaged a weaker result, proving that five colours always work.
The eventual approach was to show that a smallest map needing five colours cannot exist. Heinrich Heesch in Germany developed computer methods in the 1960s and 1970s but could not get enough supercomputer time. Two Illinois mathematicians, Kenneth Appel and Wolfgang Haken, took up the idea and in June 1976 announced success: every map must contain one of a finite set of patterns, each of which can be shrunk away. The computer checked 1,834 such patterns over more than a thousand hours, while Haken's daughter Dorothea Blostein helped verify over 400 pages of hand-checked microfiche. The department's postmark proclaimed that four colours suffice.
Many mathematicians were uneasy. Ian Stewart called the result a kind of monstrous coincidence, and rumours of an error circulated in the 1980s until Appel and Haken published corrections in 1989. A 1997 team cut the patterns to 633, and in 2005 Georges Gonthier verified the whole theorem with general-purpose proof-checking software.
Source: Four color theorem
