The four color theorem and why its proof caused a stir

The four color theorem states that no more than four colors are needed to color the regions of any map so that no two adjacent regions share a color. Adjacent regions must share a border of non-zero length, so touching at a single corner does not count. The 1976 proof by Kenneth Appel and Wolfgang Haken was controversial because it was the first major theorem proved with extensive computer assistance, and no human could check every step by hand. According to [en.wikipedia.org](https://en.wikipedia.org/wiki/Four_color_theorem), the proof has since gained wide acceptance, although some reservations remain. [1]

The problem was first conjectured in 1852 by Francis Guthrie. Many well-known mathematicians worked on it over the next century, and there were many incorrect proofs, according to [microsoft.com](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/gonthier-4colproof.pdf). Percy Heawood exposed a hole in an original proof and showed that five colors always suffice. That left the answer as either four or five. As [scientificamerican.com](https://www.scientificamerican.com/article/how-a-doodlers-problem-sparked-a-controversy-in-math/) explains, nobody could find a map needing five colors, but because there are infinitely many maps, they could not all be tested. The key step was reducing the problem to a finite set of cases, though that set was still far too large for a person to process. [2] [3]

Appel and Haken programmed a computer to check the cases, which took more than 1,000 hours of computer time. Reactions were mixed. [scientificamerican.com](https://www.scientificamerican.com/article/how-a-doodlers-problem-sparked-a-controversy-in-math/) reports that some colleagues celebrated, while others disliked computers encroaching on human ingenuity. It also reports that the New York Times at first declined to cover the announcement because earlier proofs had all been false. [3]

Several distinct objections were raised. One was philosophical: whether a proof that humans cannot verify counts as a proof at all. Another was practical. Computer programs are error-prone and hard to relate precisely to a mathematical statement, and the manual part of the analysis, about 10,000 cases, had several small errors, as the [microsoft.com](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/gonthier-4colproof.pdf) paper describes. A third concerned style. Ian Stewart found the proof unsatisfying, writing that the answer appears as a kind of monstrous coincidence, and H. S. M. Coxeter thought it very unlikely anyone could reduce it to an ordinary proof, according to [en.wikipedia.org](https://en.wikipedia.org/wiki/Four_color_theorem). The [ams.org](https://www.ams.org/publicoutreach/feature-column/fcarc-color1) column notes the original proof also had errors that were later corrected. [2] [1] [4]

In the mid-1990s, Neil Robertson, Daniel Sanders, Paul Seymour, and Robin Thomas produced a more streamlined proof that needed less computer checking but followed a similar approach. [ams.org](https://www.ams.org/meetings/national/nationalpast/wilson-jmm2003) says no serious problems have ever been found in the Appel-Haken proof, and that most mathematicians accept the newer proof without reservation. A later version reduced the configurations to 633. In 2005, Georges Gonthier verified the theorem with general-purpose proof-checking software, which removed the reliance on manually checked arguments and custom programs, per [microsoft.com](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/gonthier-4colproof.pdf). [5] [1] [2]

One complaint remains. According to [scientificamerican.com](https://www.scientificamerican.com/article/how-a-doodlers-problem-sparked-a-controversy-in-math/), no proof without computers is known, and a program that checks many configurations does not explain why four colors always suffice. Mathematicians are still looking for a more illuminating proof. [3]