Kenneth Appel (1932-2013) together with Wolfgang Haken, proved the four color theorem and broke new ground in using a computer to complete the proof. For the first time a computer played a major role in proving a major mathematical theorem.

The four color theorem states that if you only need four colors to color a 2D map so that no two adjacent regions or countries have the same color. When you try it out on a real map it seems fairly obvious, but proving it turned out to be very hard.

Credit:Inductiveload

The five color theorem has a short proof, but getting the number of colors down to four involved considering lots of possible ways that countries could share borders. It seemed to be an impossible combinatoric problem and despite some false proofs in 1852 the problem was unsolved when Appel and Haken decided to tackle the enumeration using a computer in 1976. 

As the New York Times reported it:

"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."

This was not a proof that was liked by all mathematicians. The use of the computer resulted in a proof that could not be checked by an unaided human. 

What if there was a bug in the program?

Mathematics is pure logic, and you can check the logic of a proof by reading the paper, but software is buggy - bringing computers into mathematics brings bugs with it. Many were also upset by the idea that a computer helped with the proof in that it was not an compact, elegant, proof that allowed you to get insights into the workings of the problem. In short, the computer-aided proof was not beautiful. It was a huge shock for many mathematicians at the time to have to move over and allow a computer to take part in mathematics. There was a feeling at the time, and perhaps there still is, that the proof was a temporary matter and soon a real mathematician would step up and provide a "real" proof.

Even Appel and Haken agreed, in a 1977 interview, that it was not "elegant, concise and completely comprehensible by a human mathematical mind".

Even today many mathematicians have their reservations about the proof and there have been attempts to simplify it, but so far they all involve computers. Mathematicians are still searching for something that would look more like an elementary proof. 

Appel and Haken's proof may be the most controversial in mathematics but it also put the computer into pure mathematics. 

Kenneth Appel died on April 19, 2013 at the age of 80.