The Use of the Computer in the Proof of the Four Color Theorem
K. I. Appel · 2016
M y colleague Wolfgang Haken told me that his son Armin, while a graduate student at Berkeley, was asked in 1977 to give a talk on our proof of the Four Color Theorem.1 Armin explained that the proof consisted of a rather short theoretical section, four hundred pages of detailed checklists showing that all relevant cases had been covered, and about 1,800 computer runs totaling over a thousand hours of computer time. His audience was split into two camps, largely by age. The older listeners asked, How can you believe a proof that makes such heavy use of the computer? The younger listeners asked, How can you believe a proof that depends on the accuracy of 400 pages of hand verification of detail? I would like to discuss several aspects of the questions raised. In a sense the computer has introduced into mathematics the idea of verification of results as happens in the natural sciencesvia replicable experiments. To the nonmathematician this has the effect of destroying the image of mathematics as a field in which problems are solved and solutions communicated with absolute assurance on