Motivation and history

It's not unusual for an open problem in mathematics to motivate signifi- cant research. One of the touchstone problems of modern combinatorics and graph theory was the Four Color Problem, now the Four Color Theorem after its resolution by Appel and Haken in 1976 [1]. This problem, which dates to a letter Francis Guthrie wrote to his brother Frederick in 1852, asks if it is always possible to color the regions of a map with four (or fewer) colors so that no two adjacent regions receive the same color. This is obviously important when you are looking at a map – you don't want regions (countries or states) that share a border to receive the same color.

Appel and Haken's proof was noteworthy for two reasons:

• It resolved (in the affirmative) a 125 year-old conjecture.

• It was the first significant mathematical proof that made essential use of a computer.

In fact, Appel and Haken needed more than 1000 hours of computer time to complete the case checking involved in their proof. A more recent proof [28], modeled on the same approach, but streamlined, dramatically reduces the number of cases to check. But even this new proof uses a computer in an essential way to check cases.

Although the original problem is phrased in terms of coloring regions in a map, you can turn the entire enterprise into coloring vertices of a graph.