Kenneth Appel: His Computer Program Was A Breakthrough in the Concept of Proof

Kenneth Appel. 1932 – 2013

Kenneth Ira Appel was born on October 8, 1932, in Brooklyn, New York, USA. He earned his Bachelor of Science degree in mathematics from Queens College in 1953. Appel went on to pursue his graduate studies at the University of Michigan, where he completed his Ph.D. in mathematics in 1959. His doctoral thesis was on the subject of differential equations. After completing his Ph.D., Appel held various academic positions, including teaching at the University of Illinois.

At the University of Illinois at Urbana-Champaign, he spent the majority of his academic career, where he made his most significant contribution. In 1852, Francis Guthrie had conjectured that no more than four colors are required to color the regions of any map so that no two contiguous regions have the same color. However, he couldn’t construct a proof. The problem was given to the mathematician Augustus de Morgan who tried unsuccessfully to prove what became known as the Four Color Conjecture. 

In 1976, after almost a century of failed efforts by some of the greatest mathematicians, Kenneth Appel and Wolfgang Haken, two mathematicians at the University of Illinois at Urbana-Champaign proved the conjecture with the aid of a computer. They used conventional mathematical techniques to reduce the number of possible exceptions to 1936 configurations which were then run through a computer program to be tested. After reams of computer output, no counterexamples were found, i.e., no possible maps could be constructed that required more than four colors, thus proving the Four Color Conjecture!

On the announcement of their breakthrough, the New York Times wrote in 1976:

Now the four-color conjecture has been proved by two University of Illinois mathematicians, Kenneth Appel and Wolfgang Haken. They had an invaluable tool that earlier mathematicians lacked—modern computers. Their present proof rests in part on 1,200 hours of computer calculation during which about ten billion logical decisions had to be made. The proof of the four-color conjecture is unlikely to be of applied significance. Nevertheless, what has been accomplished is a major intellectual feat. It gives us an important new insight into the nature of two-dimensional space and of the ways in which such space can be broken into discrete portions.

A widespread outcry was heard in the mathematics community by members who objected, saying that this was not a proof, because it did not consist of a sequence of logical statements that could be checked line by line in the traditional fashion. It was possible, the objectors claimed, that there was a flaw in the computer program or that the computer itself had not processed the algorithms correctly. The quest for certainty that had motivated the creation of the axiomatic system was now compromised. Simpler proofs followed in the ensuing decades, but all of them required the use of the computer to process all the possible exceptions. The computer as an intellectual aid had challenged the concept of proof that had remained virtually intact for over two millennia. Proof as a holistic understanding of how the statement of a theorem follows from the basic axioms had surrendered some territory to faith in a computer output. Prior to the computer revolution, proof was something that required nothing external to the human brain. It was becoming apparent that the superior number-crunching skills of the new technology would require mathematicians to incorporate the computer as part of their cognition.

After he and Wolfgang Haken proved the Four Color Theorem, Kenneth Appel continued his work in graph theory and computational mathematics. He continued to make significant contributions to other areas of mathematics, including the theory of computational complexity and algorithms.

Appel retired from the University of Illinois in 2003, and passed away ten years later, on April 19, 2013, in Dover, New Hampshire, at the age of 80. Kenneth Appel’s work, particularly his groundbreaking proof of the Four Color Theorem, had a lasting impact on the field of mathematics. His use of computer-assisted methods in mathematical research paved the way for new approaches to solving complex mathematical problems, and his contributions continue to be influential in the field.

In response to the controversy over the concept of a computer-based mathematical proof, Kenneth Appel once observed: The computer was, to the best of my feelings about the subject, not thinking like a mathematician, and it was much more successful, because it was thinking not like a mathematician.

Verified by MonsterInsights