Every flat map needs at most four colours.
Any map drawn on the plane can be coloured with at most four colours so that no two regions sharing a border get the same colour. The Explorer lets you build maps and watch a backtracking colouring algorithm assign at most four colours — region by region, with the smallest valid choice each time.
While colouring a map of the counties of England, the young Francis Guthrie noticed that four colours always seemed to suffice. He asked his brother Frederick, who asked their teacher Augustus De Morgan, who asked everyone. The conjecture looked harmless — and stumped mathematicians for 124 years. Several published proofs (Kempe 1879, Tait 1880) turned out to contain subtle gaps that nobody spotted for over a decade.
Three colours are demonstrably not enough — four mutually adjacent regions can already be drawn in the plane (think of three countries meeting at a corner with a fourth surrounding them). The five-colour theorem, due to Heawood in 1890, is provable in a page using Euler's formula V − E + F = 2 and a careful degree argument. Closing the gap from five down to four is what took another eighty-six years.
Kenneth Appel and Wolfgang Haken at the University of Illinois reduced the problem to a finite list of 1834 "unavoidable configurations" — and then showed each one is reducible. Their proof ran on an IBM 370 for around 1200 hours. Many mathematicians refused to accept it: a proof a human cannot read in its entirety, they argued, is not a proof. The University of Illinois mathematics department's outgoing mail was franked with "Four Colors Suffice" for years.
In 1996 Robertson, Sanders, Seymour and Thomas simplified the proof to 633 configurations and a cleaner discharging argument. In 2005 Georges Gonthier mechanised the entire proof inside the Coq proof assistant — every logical step, including the case analysis, machine-verified end to end. The theorem now powers frequency assignment in cellular networks, register allocation in compilers, and scheduling and timetabling problems wherever conflicts form a planar graph.
The chromatic number χ of a map is the smallest number of colours that suffice. Two colours are enough for any tree-like layout; three suffice for an even cycle of regions; four is forced as soon as four regions become mutually adjacent. The theorem says: you never need a fifth.
How and where this technique lives in the world today.
Topics in the same vein.
