To celebrate the 40th anniversary of the proof of the Four Color Theorem, and as a part of the 2017 sesquicentennial celebration of the founding of the University of Illinois, the Illinois Mathematics Department will hold a Four Color Fest. This event, to be held November 2-4, 2017, will be a multi-day event celebrating the mathematical, historical and cultural significance of Appel and Haken’s achievement.
Schedule of Events
Thursday, November 2, 2017
- 4 pm, 314 Altgeld Hall
Lecture: Four colors suffice
Robin Wilson (Professor Emeritus of Pure Mathematics at the Open University and at Gresham College, London)
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.
Wilson is President of the British Society for the History of Mathematics,
and the author of "Four Colours Suffice: How the Map Problem Was Solved."
5-6 pm Reception, 239 Altgeld Hall
Friday, November 3, 2017
- 4 pm, Spurlock Museum Auditorium
Lecture: Graph coloring and machine proofs in computer science, 1977-2017
Andrew Appel (Eugene Higgins Professor of Computer Science at Princeton University)
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.
- Reception 5-7 pm, Ballroom, Alice Campbell Alumni Center
Saturday, November 4, 2017
- 10 am - noon, Ballroom in Alice Campbell Alumni Center
Illinois Geometry Lab hosts an open house with Four Color Theorem-related activities for K-12 students and community.
- Math Meets Music: a special event with musical entertainment, an interesting program, food and beverages. Registration and fee required to attend.
- 7:30 pm, Music Building Auditorium
Concert: A Portrait in Four Colors
The featured instrument of the evening will be the Haken Continuum, invented by Wolfgang Haken’s son and UI Electrical and Computer Engineering faculty member Lippold. Continuum will be played by internationally renowned musician Rob Schwimmer, traveling from New York City for this event. Mr. Schwimmer will be joined by UI faculty musicians Larry Gray (bass), William Moersch (percussion), Rudolf Haken (electric viola), and pianist Whitney Ash. Program will include classical, jazz, blues, and rock genres (the synesthetic 4 colors) as well as original compositions and improvisations - a "Portrait in Four Colors" (with a nod to Charles Mingus' jazz classic Self Portrait in Three Colors).
These events are sponsored by
Department of Mathematics
Center for Advanced Study
Department of Statistics
Department of Electrical and Computer Engineering
School of Music
We also acknowledge the support of the Department of Computer Science and the University Archives.
Four Color Theorem
In 1976, two mathematicians at the University of Illinois, Kenneth Appel and Wolfgang Haken, announced the solution to the Four Color Problem. Originally posed by Francis Guthrie in 1852, the Four Color Problem conjectures that four is the smallest number of colors needed to color the regions of an arbitrary map in such a manner that any two adjacent countries are painted with different colors.
Appel and Haken’s resolution of the Four Color Problem was remarkable both for its mathematical and historical significance as the solution to a long-standing problem with an extremely simple formulation, and also for the method of proof. In fact their proof, which made extensive use of computing technology, was the first mathematical proof to rely in an essential fashion on the use of computers.
Published in 1977 in the Illinois Journal of Mathematics, the Appel-Haken Four Color Theorem is one of the signature achievements of the University of Illinois Department of Mathematics and a landmark result in geometry, graph and network theory, and computer science.