A student’s question about county maps
The claim is a specific, checkable one about maps: however a plane is divided into regions, such as the counties on a map, no more than four colours are ever needed to colour every region so that no two regions sharing a border of any real length end up the same colour. Francis Guthrie first noticed this while colouring a map of English counties on 23 October 1852, and passed the puzzle to the mathematician Augustus De Morgan through his brother, since neither of them could immediately see why it should be true rather than merely usually true. The conjecture sounds almost too simple to be difficult, since drawing test maps by hand rarely produces a case needing a fifth colour, but proving that no such case could ever exist, across every possible map, resisted mathematicians for well over a century.
A proof that stood for eleven years
Kenneth Appel and Wolfgang Haken, working with John Koch, finally proved the theorem in 1976 using a strategy built around reducing the effectively infinite variety of possible maps to a large but finite list of unavoidable configurations, 1,834 of them in the original proof, later trimmed to 1,482. Using a method called discharging to guarantee that every possible map must contain at least one of these configurations, they then had a computer check that each configuration could indeed be reduced to a smaller, already-colourable case, a verification process that consumed more than 1,000 hours of computer time. The proof was announced on 21 June 1976, and its method, rather than its conclusion, was what made it immediately controversial: it was the first major mathematical theorem whose proof no human being could check from beginning to end without a computer’s help.
Over a thousand hours of computer time
Earlier attempts at a proof had not fared well under scrutiny, which made the 1976 announcement’s own eventual acceptance meaningful rather than automatic. Alfred Kempe published a proof in 1879 that was widely accepted for eleven years before Percy Heawood identified a genuine flaw in it in 1890, and a separate attempted proof by Peter Guthrie Tait in 1880 was similarly disproved by Julius Petersen in 1891. Against that history, the computer-assisted proof has itself been substantially reinforced rather than merely repeated: a team including Robertson, Sanders, Seymour and Thomas reduced the required configurations to 633 by 1997 using an improved and more efficient method, and Georges Gonthier and Benjamin Werner formally verified the theorem in 2005 using the Coq proof-assistant, a step that removed the need to trust the original, informally written verification programs and required checking only the trusted core logic of the proof-assistant software itself.
A proof nobody could read start to finish
What did not survive scrutiny cleanly was the original 1976 proof in its first form. In the early 1980s, a graduate student named Ulrich Schmidt found genuine errors in the discharging procedure while working on his master’s thesis, and Appel and Haken had to publish a full 1989 volume addressing and correcting these problems rather than simply standing behind the original announcement. The deeper unresolved tension, which corrections to specific errors do not remove, is philosophical: mathematicians including Ian Stewart and H.S.M. Coxeter expressed real discomfort with a proof whose structure offered no insight into why the result is true, describing it as resembling a monstrous coincidence rather than an illuminating argument, a concern about mathematical understanding that persists even now that the theorem’s truth is not seriously doubted.
Errors found, and fixed, in the 1980s
The theorem’s significance runs beyond map colouring itself, because it marked the point at which a major, previously unsolved problem in pure mathematics was resolved through a method, exhaustive computer checking, that no other landmark proof had relied on before. That precedent opened a genuine methodological question that mathematics has had to keep answering since: whether a proof too large for any person to check by hand should count as a proof in the same sense as one a mathematician can follow line by line, and how much confidence formal verification software like Coq can supply in place of human comprehension. The theorem also motivated further mathematical investigation, including work connected to the Hadwiger conjecture from 1943 and generalisations of map colouring to more complex surfaces, where shapes such as a torus or a Klein bottle require as many as nine colours rather than four.
Verified by a proof-checking program
Yes, and it is worth reading precisely because the interesting part is not the theorem’s statement, which is genuinely simple, but the argument over what counts as a legitimate mathematical proof that its resolution provoked. The specific numbers involved, the 1,834 original configurations, the eleven years Kempe’s flawed proof went unchallenged, the eventual reduction to 633 cases and the 2005 formal verification, turn what could be a dry methodological dispute into a traceable sequence of real events with real stakes for how mathematics gets done. Anyone who assumes mathematical proof is a purely human, purely intuitive activity will find this a useful and specific case where that assumption had to bend.