The Four-Color Problem

In 1976, the Four-Color Problem was solved: every map drawn on a sheet of paper can be colored with only four colors in such a way that countries sharing a common border receive different colors. This result was of interest to the mathematical community since many mathematicians had tried in vain for over a hundred years to prove this simple-sounding statement. Yet among mathematicians who were not aware of the developments leading to the proof, the outcome had rather dismaying aspects, for the proof made unprecedented use of computer computation; the correctness of the proof cannot be checked without the aid of a computer. Moreover, adding to the strangeness of the proof, some of the crucial ideas were perfected by computer experiments. One can never rule out the chance that a short proof of the Four-Color Theorem might some day be found, perhaps by the proverbial bright high-school student. But it is also conceivable that no such proof is possible. In this case a new and interesting type of theorem has appeared, one which has no proof of the traditional type.