by the Department of Mathematics,
University of Illinois
To celebrate the 40th anniversary of Kenneth Appel and Wolfgang Haken’s proof of the Four Color Theorem, and as part of the 2017 sesquicentennial celebration of the founding of the University of Illinois, the Illinois Mathematics Department held a Four Color Fest on November 2–4, 2017.
The event featured lectures by guest speakers(Open University and Gresham College) and Andrew Appel (Kenneth Appel’s son and Eugene Higgins Professor of Computer Science at Princeton University), as well as remarks by other colleagues and family members of the two mathematicians.
The lectures were recorded and made available via YouTube, and the reader can find here (in order of their presentation) the links to each of them:
- Video lecture by Robin Wilson (Open University and Gresham College): Mathematics in Science and Society Lecture: “Lewis Carroll in Numberland”.
- Video lecture
by Robin Wilson,
author of Four Colors Suffice: How the Map Problem Was
Solved (Princeton University Press, 2014).
Abstract: In this talk I present the history and solution of the four-color problem: Can every map be colored with just four colors so that neighboring countries are colored differently? The solution took 124 years to find, and used 1200 hours of computer time. But what did it involve, is it really a solution, and what role did the University of Illinois play in solving the problem? This illustrated lecture is open to anyone interested in this fascinating (and colorful) topic.
The slides from this can be talked can be accessed in this volume; see .
- Video lecture
by Andrew Appel:
“Graph coloring and machine proofs in computer science, 1977–2017”.
Abstract: The Four Color Theorem of Kenneth Appel and Wolfgang Haken (1976) was proved and checked with the assistance of computer programs, though much of the proof was written (and refereed) only by humans. Contemporaneously, Edinburgh LCF (Logic for Computable Functions) was developed by Robin Milner — a system for proofs written by humans (with computer assistance) but completely checked by computer, with particular application to proofs about computer programs. These two developments, and their convergence, have had significant impact on computer science, and my own research career: graph-coloring algorithms for register allocation in compilers, functional programming languages, fully machine-checked proofs of mathematical theorems, fully machine-checked proofs of software systems. One result at the intersection of all these is a machine-checked proof of correctness of a program that does register allocation by graph-coloring, using an algorithm related to one used in every four-color proof (and attempted proof) since 1879.
The slides from this talk can be accessed in this volume; see .
- Remarks and reminiscences by colleagues and family of Appel and Haken.