by David H. Bailey and Jonathan M. Borwein
Kenneth Appel, who along with Wolfgang Haken, in 1976 gave the first proof of the four-color theorem, died on April 19, 2013, at the age of 80.
Appel was employed as an actuary and also served in the U.S. Army before completing his Ph.D. in mathematics in 1959. After working for a few years at the Institute for Defense Analyses, in 1969 he joined the University of Illinois, where he did research in group theory and the theory of computation.
The four-color theorem is the assertion that, under certain reasonable conditions (such as that no component region is disconnected like Michigan), only four colors suffice to color any planar map such that no two adjacent regions have the same color.
This fact was first conjectured in 1852 by Francis Guthrie, who, while attempting to color a map of the counties in England, noticed that only four different colors were needed. As it turns out, Guthrie’s brother Frederick was a student of Augustus De Morgan of set theory fame, who posed the question to the mathematical community. For nearly 100 years, numerous “proofs” were proposed, only later shown to be incorrect. As Wikipedia describes:
There were several early failed attempts at proving the theorem. One proof was given by Alfred Kempe in 1879, which was widely acclaimed; another was given by Peter Guthrie Tait in 1880. It was not until 1890 that Kempe’s proof was shown incorrect by Percy Heawood, and 1891 Tait’s proof was shown incorrect by Julius Petersen — each false proof stood unchallenged for 11 years.1
Kempe’s ideas as corrected by Percy Heawood did show that five colors suffice by using Kempe chains. This stood as the best result for almost a century. During the 1960s and 1970s, Heinrich Heesch developed modern computer-based proof methods. He looked into the four-color theorem, but was unable to obtain sufficient supercomputer time — such as it was in 1970 — to pursue the problem.
Other researchers, among them Kenneth Appel and Wolfgang Haken at the University of Illinois Urbana-Champaign, adopted Heesch’s results within their own computer programs. Appel and Haken’s approach was to show (i) with computational assistance that any counterexample to the four-color theorem must belong to a set of 1936 unavoidable configurations, later reduced to 1476. Then (ii) their computer program checked each of these cases, and, on 21 June 1976, they announced their achievement. Since then the postmark for the Department of Mathematics at the university has been “Four colors suffice.”
Their work attracted considerable controversy and scrutiny, both within the mathematical philosophy world and from research mathematicians. There were objections that the proof amounted to “the computer says,” and some asked how this differed from “it is true because von Neumann says it is.” There were justifiable concerns about its rigor, and grouchy rejections by computational luddites.
Within a few years, Ulrich Schmidt at RWTH Aachen found an error in the procedure used by Appel and Haken. In 1989, Appel and Haken responded with a manuscript “Every planar map is four-colorable,” which explained Schmidt’s discovery and included corrected results.
Research continued in computer-based methods for map coloring. In 1996, Robertson, Sanders, Seymour and Thomas published a new scheme for coloring an arbitrary map in time that increases only quadratically in the number of regions. With this scheme, they were able to reproduce the Appel–Haken result, but again their proof is not practicable to be checked by hand (although it was much more streamlined). Finally, in 2005, Werner and Gonthier of Microsoft Research were able to prove the result using the Coq interactive theorem prover, which, although still a computer-based proof, nonetheless represented a significant milestone for formal proof engines.
It is ironic and appropriate that as Chandler Davis has wryly observed, concerns raised about the use of computers in mathematics in the 1970s were put to bed twenty-five years later by the careful use of computers.
It is interesting to reflect on how far computer-based mathematics has come since the Appel–Haken result. As noted, the original result drew considerable criticism from the mathematical community because of its utilization of a computer. This criticism is perhaps not too surprising, since the conventional wisdom at the time was that “real mathematicians don’t compute.” Indeed, computers were disdained as a tool for accountants and engineers, certainly not for theoretical mathematicians.
But it is clear that this groundbreaking work spurred many other mathematicians to begin looking at how the computer could be used as a tool in real mathematical research.
Not too many years later, the discipline of experimental mathematics was born, with dozens and later hundreds of serious mathematical papers utilizing recent computer technology to gain insight and intuition, to discover new patterns and relationships, to use graphical displays to suggest underlying mathematical principles, to test and especially to falsify conjectures, to explore a result to see if it is worth formal proof, to suggest approaches for formal proof, to replace lengthy hand derivations with computer-based derivations, and to confirm analytically derived results.
Along this line, formal methods are being used much more widely to confirm and certify proofs — see the November 2008 issue of the Notices of the American Mathematical Society. For example, in 1998 Thomas Hales announced a proof of the Kepler conjecture (namely, the assertion that the most space-efficient method to stack spheres is the scheme we see in use for oranges in the grocery store). His proof was published in 2005 in the Annals of Mathematics after running into a headwind, some of which was justified as it used uncertifiable computations. In response, Hales is close to finishing a proof of the Kepler conjecture result using rigorous computer-based formal methods.2 Some of the tools developed will be very useful elsewhere.
The field of computational and experimental mathematics has certainly blossomed in the past four decades. Thus, it is entirely appropriate that we give honor to Kenneth Appel, one of its true pioneers.
We should add that while it would be lovely to see a fully human and accessible proof, there is no particular reason to think one exists.
Additional details are available in the Wikipedia article on Appel, the Chicago Sun-Times obituary of Appel, the Wikipedia article on the four color theorem and Robin Wilson’s 2002 book Four Colors Suffice.
