You are the lead cartographer for Blobland, a country which has a lot of states. For the sake of aesthetics, you hope to color the states that share a border with different colours. How many colours do you need? An obvious solution is to colour all the different states with different colours, but that would require a lot of colours. Can you do better? It is easy to see that there exists a map that requires four colours. Are there maps that need more than that?
This question, first posed by Francis Guthrie, a British cartographer in 1852, puzzled some of the most famous mathematicians in the late-19th and early-20th centuries. It was finally answered in 1976 by Kenneth Appel and Wolfgang Haken in a two-part monstrosity of a paper that contained 700 pages of hand calculations and thousands of cases solved by a computer program. This (in)famous “proof” divided mathematicians of the time into two groups - those who did not believe that the cases solved by the cases where error-free and those who did not believe that the cases solved by hand were error-free.
The proof got the attention of the philosophical community as well. In particular, they were concerned with the following question: what is a proof? If a set of statements are not surveyable (which Appel’s and Haken’s result was surely not), can it really be considered a proof?
At the Mini-Course on Computation organized by Chi-Ning at Harvard GSAS, I delivered a talk on January 12, 2022 to a general audience on this topic. In this talk, I addressed the history of the problem, some key components of the eventual proof, and its philosophical implications. Here is the recording of the talk and here are its slides. If you find any typos, mistakes, or just want to talk about this topic, email me!