why any map needs only four colors

The Mechanism

*The four-color theorem* states that any map drawn on a plane can be coloured with at most four colours such that no two adjacent regions share a colour. The conjecture was first noticed in *October 1852* by *Francis Guthrie* (1831-1899), a 21-year-old recent graduate of *University College London* who was colouring a map of the counties of England. Guthrie mentioned the observation to his younger brother *Frederick Guthrie*, then a chemistry student at UCL, who passed it on to their mathematics professor *Augustus De Morgan*. De Morgan wrote a famous 23 October 1852 letter to Sir *William Rowan Hamilton* in Dublin describing the conjecture. Hamilton was not interested. The problem stayed in private correspondence for two and a half decades until *Arthur Cayley* raised it before the London Mathematical Society in 1878. The next year *Alfred Bray Kempe*, a London barrister and amateur mathematician, published what he believed was a proof in the *American Journal of Mathematics*; a second proof followed from the Glasgow physicist *Peter Guthrie Tait* in 1880. Both proofs were accepted as correct for eleven years. In *1890*, *Percy John Heawood* — a young Durham mathematician — found a subtle flaw in Kempe's *Kempe chain* argument that could not be repaired; what survived of Kempe's reasoning yielded only the weaker *Five Colour Theorem* (every planar map can be 4-coloured was downgraded to 5-coloured). The four-colour conjecture went back to being open, and stayed open for another eighty-six years. The route to a proof was opened by the German mathematician *Heinrich Heesch*, who through the 1950s and 1960s developed the two essential ingredients: an *unavoidable set* (a finite list of local map-configurations such that every planar map must contain at least one of them) and a *reducibility test* (a procedure to show that, if a map contains a given configuration, the map can be reduced to a smaller map with the same colouring number). If a finite unavoidable set of reducible configurations could be exhibited, the theorem would follow. Heesch's *discharging method* — borrowed from electrostatics — gave a systematic technique for searching for unavoidable sets. By the late 1960s Heesch had reduced the conjecture in principle to the inspection of a few thousand configurations, but the case analysis required by hand was prohibitive. In *1972*, *Kenneth Appel* (1932-2013) and *Wolfgang Haken* (1928-2022), both at the *University of Illinois at Urbana-Champaign Department of Mathematics*, took up the problem with the explicit intention of using a computer. Haken had been Heesch's pupil at Kiel before emigrating; Appel had been an algebraist at the Institute for Defense Analyses before joining Illinois in 1961. They spent four years refining the discharging procedure and the unavoidable-set construction, repeatedly redesigning the configurations to make them small enough to test for reducibility with the available mainframe time. They worked with the Illinois undergraduate *John Koch*, who wrote the reducibility-testing software. By the summer of *1976* they had a candidate unavoidable set of *1,834 reducible configurations*. The verification ran on the *University of Illinois IBM mainframe* — one of two IBM 370 systems on campus — for *over 1,200 hours of CPU time* across the spring and early summer. On *21 June 1976* Appel and Haken announced the proof complete. From that day forward, the Department of Mathematics in Urbana-Champaign stamped its outgoing mail with the postmark *FOUR COLORS SUFFICE*. The reaction in the mathematics community was sharp. The proof was, in a precise sense, the *first major theorem in mathematical history whose verification no single human being could carry out*; the case analysis ran to thousands of pages of computer printout that could not be checked by hand in any reasonable time. *Paul Halmos* argued at length that what Appel and Haken had produced was an empirical result, not a proof; the philosopher *Thomas Tymoczko* in 1979 wrote a much-cited paper, *"The Four-Colour Problem and Its Philosophical Significance,"* arguing that the proof represented a fundamentally new kind of mathematical knowledge that depended on a non-mathematical instrument. *Daniel Cohen* in 1976 published the Appel-Haken proof in the *Illinois Journal of Mathematics* (volume 21, pages 429-567) over two long companion papers; the printed paper covered the unavoidable set and the discharging procedure but referred the reader to a *400-page microfiche supplement* for the reducibility checks. The consolidation came slowly. In *1996*, *Neil Robertson*, *Daniel P. Sanders*, *Paul Seymour*, and *Robin Thomas*, at the Georgia Institute of Technology and Princeton, gave a new and substantially simpler proof — same general strategy, but with only *633 reducible configurations* in their unavoidable set instead of 1,834, and a much shorter discharging procedure. In *2005*, *Georges Gonthier* at Microsoft Research Cambridge, working from a formalisation by *Benjamin Werner* of INRIA, encoded the Robertson-Sanders-Seymour-Thomas proof in the *Coq* proof assistant — a piece of software whose own kernel is small enough to be inspected by hand. The four-colour theorem was the first major mathematical theorem ever to receive a fully *formally verified* machine-checked proof. As of 2026, every cartographer in the world can colour every map of the world's countries with at most four colours — and we know why, in a chain of inference that begins with a 21-year-old colouring English counties at his table in 1852 and ends with a Coq script compiling without error on a laptop in 2005.