The Four-Color Theorem Was the First Major Proof a Human Could Not Verify by Hand

The four-color theorem says that any map drawn on a plane can be colored with at most four colors so that no two regions sharing a border get the same color. Francis Guthrie posed it in 1852 while coloring a map of British counties; his brother Frederick passed it to the mathematician Augustus De Morgan, who could not crack it. For 124 years, it remained one of the most famous open problems in graph theory.

Kenneth Appel and Wolfgang Haken at the University of Illinois finished a proof in June 1976. Their strategy followed a long line of work by Heinrich Heesch and others: identify a finite set of 'reducible configurations' that any minimal counterexample would have to contain, then show that every planar graph contains at least one of those configurations and so cannot be a counterexample. The hard part was the size of the set. Appel and Haken's catalog ran to 1,936 configurations. Each had to be checked for reducibility — a calculation involving extensive case analysis no human could complete by hand.

They ran the verification on an IBM System/360 at the university's computing center. About 1,200 hours of CPU time later, the proof was complete. They announced it in a 1976 talk at the University of Toronto, then published the full account in two long papers in the Illinois Journal of Mathematics in 1977.

The response was uneasy. Mathematicians could read the human portion in weeks, but no one could check the computer's case analysis except by writing more software. Some considered it a proof; some thought a result no one had personally verified did not deserve the word. The debate forced acceptance of a new kind of object: theorems whose justification depends on machines we trust. Robertson, Sanders, Seymour, and Thomas produced a streamlined re-proof in 1996.