Four colours suffice to colour any map so that no two regions sharing a border have the same colour. It was conjectured in 1852, resisted proof for over a century, and was finally settled in 1976 by a computer checking cases no human could verify by hand. That is why it is remembered.
Francis Guthrie noticed in 1852, while colouring a map of English counties, that four colours seemed always to be enough. He asked whether this was always true, and the question reached Augustus De Morgan, who circulated it.
The statement is easy. Regions must be connected, so a country with an exclave does not count, and regions meeting at a single point do not share a border.
Three colours are demonstrably insufficient, which a simple arrangement of four mutually adjacent regions shows. Five colours were proved sufficient by Percy Heawood in 1890, by an argument that is not difficult. The gap between four and five took another eighty-six years.
Alfred Kempe published a proof in 1879 and it was accepted. He was elected to the Royal Society partly on the strength of it.
Heawood found the error in 1890. Kempe's argument used chains of alternating colours to recolour parts of a map, and one case in his analysis did not work as claimed.
The failure was productive. Kempe's chains remained useful and Heawood salvaged the five-colour theorem from the wreckage. But an accepted proof standing for eleven years, in a problem this well known, is worth remembering when a new proof of something famous appears.
Kenneth Appel and Wolfgang Haken at the University of Illinois proved it in 1976, using a strategy developed over decades by others.
The approach has two parts. First, produce an unavoidable set: a collection of configurations such that every possible map must contain at least one of them. Second, show every configuration in that set is reducible: if the rest of the map can be four-coloured, the configuration can be too.
Together these give a proof by contradiction. A smallest counterexample must contain a configuration from the unavoidable set, that configuration is reducible, so the counterexample is not minimal, so no counterexample exists.
Appel and Haken's unavoidable set contained 1,936 configurations. Checking each for reducibility required around 1,200 hours of computer time, which was a great deal in 1976.
The Illinois postmark carried the phrase "four colors suffice" afterwards.
The reaction was uncomfortable and the discomfort was serious rather than reactionary.
No human could check the computation. A proof had always been something a mathematician could in principle verify by reading it, and this one required trusting a program, the compiler, and the hardware.
Objections took several forms. Some argued that a proof should explain why a result is true, and this one establishes the fact while illuminating nothing. Others noted that the program contained errors that were found and corrected, raising the question of how one would know the last had been found. Part of the original case analysis was done by hand and contained errors too.
Defenders replied that long human proofs are also error-prone, that referees rarely check every line of a hundred-page argument, and that a program can be examined by others in a way a mathematician's private reasoning cannot.
The proof was independently redone by Robertson, Sanders, Seymour and Thomas in 1996, with a smaller unavoidable set of 633 configurations and cleaner methods. It is still computer-assisted.
Georges Gonthier produced a fully machine-checked proof in 2005 using the Coq proof assistant, in which every step including the logic is verified formally by software whose own correctness is much easier to establish than that of an ad hoc program.
That is arguably a stronger guarantee than any human-verified proof of comparable length offers.
The theorem's importance is not the result, which has little application. Maps are not coloured this way in practice.
Its importance is that it was the first major theorem proved by computer, and it forced the question of what a proof is for. Since then, computer-assisted and formally verified proofs have become ordinary: the Kepler conjecture on sphere packing was settled this way, and several long human proofs have been formalised to check them.
The discomfort has largely faded, and the question underneath it has not been fully answered. A proof serves two purposes, establishing truth and producing understanding, and computer proofs are much better at the first than the second.
