In 1976, Wolfgang Haken and Kenneth Appel solved a problem that had gone unresolved for over 100 years: Is it true that every map drawn in the plane can be colored with four or fewer colors? The ease of stating the problem belied the proof that Haken and Appel provided, which to this day generates some controversy. The proof depended on the use of a computer program in an essential way. It is impossible for a person to verify every step of the proof. Like many complex proofs, the original version of the proof that Haken and Appel announced had some errors. Although they provided corrections, the fact that the proof also involved a computer added to the discomfort with which the proof was greeted. Subsequently, in 1994 a new proof of the four-color theorem appeared. This proof was the work of Neil Robertson, Daniel Sanders, Paul Seymour, and Robin Thomas. Though the proof was considerably simpler than the Haken-Appel proof, like that proof it followed an approach pioneered by Heinrich Heesch (1906-1995). Yet this proof still needed a computer to verify the many cases that arose from the strategy. Some people are skeptical that a truly short proof of the four-color problem exists.
Although resolving the four-color problem was a triumph of the human intellect, more important are the mathematical tools and ideas that emerged from its solution. New insights into many additional coloring problems emerged, as did powerful new ideas that were useful in answering questions about embeddings of graphs on surfaces. Furthermore, the investigation of coloring problems led to many applications outside of mathematics. These include scheduling of college courses and legislative committees, as well as assigning frequencies for use in cell phone traffic.