Four Color Theorem

The theorem that any map drawn on a plane can be colored with only four colors so that no two regions sharing a border receive the same color. Francis Guthrie posed the conjecture around 1852 while coloring a map of the counties of England; his brother Frederick brought it to Augustus De Morgan's attention that October. Alfred Bray Kempe announced a proof in 1879 that stood for eleven years until Percy John Heawood found a defect in it in 1890, and an independent 1880 attempt by Peter Guthrie Tait was shown flawed by Julius Petersen in 1891. Kenneth Appel and Wolfgang Haken, at the University of Illinois at Urbana-Champaign, finally proved the theorem in 1976 using an unavoidable set of reducible configurations checked by computer, roughly 1,900 configurations reduced from Appel and Haken's own working set, using around 1,200 hours of computer time; it was the first major theorem ever proved with a step that could not be verified by a human reading it line by line, which set off a genuine and lasting debate over whether such a proof counts as a proof in the traditional sense. A German student, Ulrich Schmidt, found an error in the original reducibility procedure a few years after publication, corrected within about two weeks; Appel and Haken addressed it in their 1989 book. In 1997 Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas published a simplified, still computer-assisted proof cutting the unavoidable set to 633 configurations and the discharging rules from over 300 to 32. In 2005 Georges Gonthier produced a fully machine-checked proof in the Coq proof assistant, removing reliance on any unverified custom program or unreviewable manual step.