Celebratio Mathematica

Kenneth Ira Appel

The colorful life of the four-color theorem:
A tribute to Kenneth Appel

by David H. Bailey and Jonathan M. Borwein

Ken­neth Ap­pel, who along with Wolfgang Haken, in 1976 gave the first proof of the four-col­or the­or­em, died on April 19, 2013, at the age of 80.

Ap­pel was em­ployed as an ac­tu­ary and also served in the U.S. Army be­fore com­plet­ing his Ph.D. in math­em­at­ics in 1959. After work­ing for a few years at the In­sti­tute for De­fense Ana­lyses, in 1969 he joined the Uni­versity of Illinois, where he did re­search in group the­ory and the the­ory of com­pu­ta­tion.

The four-col­or the­or­em is the as­ser­tion that, un­der cer­tain reas­on­able con­di­tions (such as that no com­pon­ent re­gion is dis­con­nec­ted like Michigan), only four col­ors suf­fice to col­or any planar map such that no two ad­ja­cent re­gions have the same col­or.

This fact was first con­jec­tured in 1852 by Fran­cis Gu­thrie, who, while at­tempt­ing to col­or a map of the counties in Eng­land, no­ticed that only four dif­fer­ent col­ors were needed. As it turns out, Gu­thrie’s broth­er Fre­d­er­ick was a stu­dent of Au­gus­tus De Mor­gan of set the­ory fame, who posed the ques­tion to the math­em­at­ic­al com­munity. For nearly 100 years, nu­mer­ous “proofs” were pro­posed, only later shown to be in­cor­rect. As Wiki­pe­dia de­scribes:

There were sev­er­al early failed at­tempts at prov­ing the the­or­em. One proof was giv­en by Al­fred Kempe in 1879, which was widely ac­claimed; an­oth­er was giv­en by Peter Gu­thrie Tait in 1880. It was not un­til 1890 that Kempe’s proof was shown in­cor­rect by Percy Heawood, and 1891 Tait’s proof was shown in­cor­rect by Ju­li­us Petersen — each false proof stood un­chal­lenged for 11 years.1

Kempe’s ideas as cor­rec­ted by Percy Heawood did show that five col­ors suf­fice by us­ing Kempe chains. This stood as the best res­ult for al­most a cen­tury. Dur­ing the 1960s and 1970s, Hein­rich Heesch de­veloped mod­ern com­puter-based proof meth­ods. He looked in­to the four-col­or the­or­em, but was un­able to ob­tain suf­fi­cient su­per­com­puter time — such as it was in 1970 — to pur­sue the prob­lem.

Oth­er re­search­ers, among them Ken­neth Ap­pel and Wolfgang Haken at the Uni­versity of Illinois Urb­ana-Cham­paign, ad­op­ted Heesch’s res­ults with­in their own com­puter pro­grams. Ap­pel and Haken’s ap­proach was to show (i) with com­pu­ta­tion­al as­sist­ance that any counter­example to the four-col­or the­or­em must be­long to a set of 1936 un­avoid­able con­fig­ur­a­tions, later re­duced to 1476. Then (ii) their com­puter pro­gram checked each of these cases, and, on 21 June 1976, they an­nounced their achieve­ment. Since then the post­mark for the De­part­ment of Math­em­at­ics at the uni­versity has been “Four col­ors suf­fice.”

Their work at­trac­ted con­sid­er­able con­tro­versy and scru­tiny, both with­in the math­em­at­ic­al philo­sophy world and from re­search math­em­aticians. There were ob­jec­tions that the proof amoun­ted to “the com­puter says,” and some asked how this differed from “it is true be­cause von Neu­mann says it is.” There were jus­ti­fi­able con­cerns about its rig­or, and grouchy re­jec­tions by com­pu­ta­tion­al lud­dites.

With­in a few years, Ul­rich Schmidt at RWTH Aachen found an er­ror in the pro­ced­ure used by Ap­pel and Haken. In 1989, Ap­pel and Haken re­spon­ded with a manuscript “Every planar map is four-col­or­able,” which ex­plained Schmidt’s dis­cov­ery and in­cluded cor­rec­ted res­ults.

Re­search con­tin­ued in com­puter-based meth­ods for map col­or­ing. In 1996, Robertson, Sanders, Sey­mour and Thomas pub­lished a new scheme for col­or­ing an ar­bit­rary map in time that in­creases only quad­rat­ic­ally in the num­ber of re­gions. With this scheme, they were able to re­pro­duce the Ap­pel–Haken res­ult, but again their proof is not prac­tic­able to be checked by hand (al­though it was much more stream­lined). Fi­nally, in 2005, Wern­er and Gonthi­er of Mi­crosoft Re­search were able to prove the res­ult us­ing the Coq in­ter­act­ive the­or­em prover, which, al­though still a com­puter-based proof, non­ethe­less rep­res­en­ted a sig­ni­fic­ant mile­stone for form­al proof en­gines.

It is iron­ic and ap­pro­pri­ate that as Chand­ler Dav­is has wryly ob­served, con­cerns raised about the use of com­puters in math­em­at­ics in the 1970s were put to bed twenty-five years later by the care­ful use of com­puters.

It is in­ter­est­ing to re­flect on how far com­puter-based math­em­at­ics has come since the Ap­pel–Haken res­ult. As noted, the ori­gin­al res­ult drew con­sid­er­able cri­ti­cism from the math­em­at­ic­al com­munity be­cause of its util­iz­a­tion of a com­puter. This cri­ti­cism is per­haps not too sur­pris­ing, since the con­ven­tion­al wis­dom at the time was that “real math­em­aticians don’t com­pute.” In­deed, com­puters were dis­dained as a tool for ac­count­ants and en­gin­eers, cer­tainly not for the­or­et­ic­al math­em­aticians.

But it is clear that this ground­break­ing work spurred many oth­er math­em­aticians to be­gin look­ing at how the com­puter could be used as a tool in real math­em­at­ic­al re­search.

Not too many years later, the dis­cip­line of ex­per­i­ment­al math­em­at­ics was born, with dozens and later hun­dreds of ser­i­ous math­em­at­ic­al pa­pers util­iz­ing re­cent com­puter tech­no­logy to gain in­sight and in­tu­ition, to dis­cov­er new pat­terns and re­la­tion­ships, to use graph­ic­al dis­plays to sug­gest un­der­ly­ing math­em­at­ic­al prin­ciples, to test and es­pe­cially to falsi­fy con­jec­tures, to ex­plore a res­ult to see if it is worth form­al proof, to sug­gest ap­proaches for form­al proof, to re­place lengthy hand de­riv­a­tions with com­puter-based de­riv­a­tions, and to con­firm ana­lyt­ic­ally de­rived res­ults.

Along this line, form­al meth­ods are be­ing used much more widely to con­firm and cer­ti­fy proofs — see the Novem­ber 2008 is­sue of the No­tices of the Amer­ic­an Math­em­at­ic­al So­ci­ety. For ex­ample, in 1998 Thomas Hales an­nounced a proof of the Kepler con­jec­ture (namely, the as­ser­tion that the most space-ef­fi­cient meth­od to stack spheres is the scheme we see in use for or­anges in the gro­cery store). His proof was pub­lished in 2005 in the An­nals of Math­em­at­ics after run­ning in­to a head­wind, some of which was jus­ti­fied as it used un­cer­ti­fi­able com­pu­ta­tions. In re­sponse, Hales is close to fin­ish­ing a proof of the Kepler con­jec­ture res­ult us­ing rig­or­ous com­puter-based form­al meth­ods.2 Some of the tools de­veloped will be very use­ful else­where.

The field of com­pu­ta­tion­al and ex­per­i­ment­al math­em­at­ics has cer­tainly blos­somed in the past four dec­ades. Thus, it is en­tirely ap­pro­pri­ate that we give hon­or to Ken­neth Ap­pel, one of its true pi­on­eers.

We should add that while it would be lovely to see a fully hu­man and ac­cess­ible proof, there is no par­tic­u­lar reas­on to think one ex­ists.

Ad­di­tion­al de­tails are avail­able in the Wiki­pe­dia art­icle on Ap­pel, the Chica­go Sun-Times ob­it­u­ary of Ap­pel, the Wiki­pe­dia art­icle on the four col­or the­or­em and Robin Wilson’s 2002 book Four Col­ors Suf­fice.