Celebratio Mathematica

To cel­eb­rate the 40th an­niversary of Ken­neth Ap­pel and Wolfgang Haken’s proof of the Four Col­or The­or­em, and as part of the 2017 ses­qui­cent­en­ni­al cel­eb­ra­tion of the found­ing of the Uni­versity of Illinois, the Illinois Math­em­at­ics De­part­ment held a Four Col­or Fest on Novem­ber 2–4, 2017.

The event fea­tured lec­tures by guest speak­ers Robin Wilson (Open Uni­versity and Gre­sham Col­lege) and An­drew Ap­pel (Ken­neth Ap­pel’s son and Eu­gene Hig­gins Pro­fess­or of Com­puter Sci­ence at Prin­ceton Uni­versity), as well as re­marks by oth­er col­leagues and fam­ily mem­bers of the two math­em­aticians.

The lec­tures were re­cor­ded and made avail­able via You­Tube, and the read­er can find here (in or­der of their present­a­tion) the links to each of them:

• Video lec­ture by Robin Wilson (Open Uni­versity and Gre­sham Col­lege): Math­em­at­ics in Sci­ence and So­ci­ety Lec­ture: “Lewis Car­roll in Num­ber­land”.
• Video lec­ture by Robin Wilson, au­thor of Four Col­ors Suf­fice: How the Map Prob­lem Was Solved (Prin­ceton Uni­versity Press, 2014).

  Ab­stract: In this talk I present the his­tory and solu­tion of the four-col­or prob­lem: Can every map be colored with just four col­ors so that neigh­bor­ing coun­tries are colored dif­fer­ently? The solu­tion took 124 years to find, and used 1200 hours of com­puter time. But what did it in­volve, is it really a solu­tion, and what role did the Uni­versity of Illinois play in solv­ing the prob­lem? This il­lus­trated lec­ture is open to any­one in­ter­ested in this fas­cin­at­ing (and col­or­ful) top­ic.

  The slides from this can be talked can be ac­cessed in this volume; see [◊].

• Video lec­ture by An­drew Ap­pel: “Graph col­or­ing and ma­chine proofs in com­puter sci­ence, 1977–2017”.

  Ab­stract: The Four Col­or The­or­em of Ken­neth Ap­pel and Wolfgang Haken (1976) was proved and checked with the as­sist­ance of com­puter pro­grams, though much of the proof was writ­ten (and ref­er­eed) only by hu­mans. Con­tem­por­an­eously, Ed­in­burgh LCF (Lo­gic for Com­put­able Func­tions) was de­veloped by Robin Mil­ner — a sys­tem for proofs writ­ten by hu­mans (with com­puter as­sist­ance) but com­pletely checked by com­puter, with par­tic­u­lar ap­plic­a­tion to proofs about com­puter pro­grams. These two de­vel­op­ments, and their con­ver­gence, have had sig­ni­fic­ant im­pact on com­puter sci­ence, and my own re­search ca­reer: graph-col­or­ing al­gorithms for re­gister al­loc­a­tion in com­pilers, func­tion­al pro­gram­ming lan­guages, fully ma­chine-checked proofs of math­em­at­ic­al the­or­ems, fully ma­chine-checked proofs of soft­ware sys­tems. One res­ult at the in­ter­sec­tion of all these is a ma­chine-checked proof of cor­rect­ness of a pro­gram that does re­gister al­loc­a­tion by graph-col­or­ing, us­ing an al­gorithm re­lated to one used in every four-col­or proof (and at­temp­ted proof) since 1879.

  The slides from this talk can be ac­cessed in this volume; see [◊].

• Re­marks and re­min­is­cences by col­leagues and fam­ily of Ap­pel and Haken.