Speaker: Steve Bellenot
Abstract. Of all the major mathematical successes from the last century, the computer assisted solution to the four color problem is the most enigmatic. The solving of the four color problem was a major goal of the graph theory community for 124 years. Its history was filled with false proofs and false counterexamples. In 1976, Appel and Haken with programming expert Koch and 1400 hours of main frame (IBM 360 and 370) computer time gave the first proof. Did the mathematics community rejoice or was it as if the Grinch had stolen Christmas? Since 1976, there have been several new proofs of the four color problem, all with computer assistance. Since 1976, another dozen or so mathematical questions have been solved with computer aid.