It’s been almost a month now since we lost one of the revolutionaries of 20th century mathematics, Dr. Kenneth Ira Appel. The obituaries in the New York Times as well as The Economist do a good job of describing his life and most famous contribution to mathematics, the computer-assisted proof of the Four Color Theorem, a result stating that any map can be colored with 4 colors without any neighboring countries sharing the same color. In this post, I will discuss his broader contribution to the way a lot of mathematics is done today, namely, in collaboration with computers.
A fact that many people tend to forget is that computers have their origins in logic and mathematics. The foundational work of the logician Alonzo Church and the mathematicians Alan Turing and John von Neumann led to the development of both the theory of computation (now a branch of computer science) and the modern computer. While technological advances allowed for the miniaturization of computers to the point where our cell phones today are faster and more powerful than the early computers which occupied entire large rooms, it was the work of these mathematicians that made it possible for computers to exist in the first place.
Soon after their first appearance, computers were put to use for solving various complex problems, mostly related to physics and engineering, such as simulating flight trajectories, predicting the dynamics of fluids, and finding optimal allocations of resources. The size and scope of problems solvable by computers grew together with the improvements in the underlying technology (often described by Moore’s Law, which says that various characteristics determining the speed of a computer double roughly every 18 months). However, mathematicians on the whole took a surprisingly long time before accepting and making use of the new technology in their work, sticking to the traditional approach of proving theorems “by hand”.
This all changed after Kenneth Appel and his co-author, Wolfgang Haken, published their 1976 proof of the Four Color Theorem, which had baffled mathematicians for almost 125 years (this is by no means a record, however, as Fermat’s Last Theorem had remained unproven for over 350 years). This proof consisted of a significant new advance that enumerated 1936 potentially problematic configurations, and the result of a large-scale computer effort checking that 4 colors suffice for all of these configurations. While initially met with significant skepticism, this proof eventually became accepted by the mathematical community, and further simplified over the years, to the point that very little doubt about the correctness of the result remains.
This early success provided the impetus for the development of entire new fields of mathematics, such as automated theorem proving and interactive theorem proving. These deal with the finding and verifying the proof of a theorem by using a formal system describing the transformations (logical steps) allowed in creating proofs. So far, a few other important problems have been solved with the assistance of a computer, including Kepler’s conjecture on the optimal packing of spheres and a problem related to the behavior of the Lorenz system of differential equations.
Many similar ideas are also used in computer algebra systems such as Maple, which have found a wide range of applications. But most importantly, mathematicians now routinely use computers to explore the validity of a statement before trying to prove it. This essentially allows many branches of mathematics to proceed by the scientific method, where a hypothesis is formulated, tested experimentally (on a computer), and refined if necessary. The final stage of writing down a proof is still usually done by the mathematician, but the preliminary stage of building intuition and narrowing down the options is now much more pleasant, since computers are much better than humans at many routine tasks such as manipulating algebraic expressions. This revolution, ushered in by Kenneth Appel’s work, will continue to permeate 21st century mathematics, and I predict that it will encompass more and more subfields.