László Fejes Tóth used the term "intuitive geometry" to describe the fields of geometry featuring problems which are simple to state and extremely hard to resolve, such as the Kepler conjecture and the four-color theorem. Problems with straightforward statements that still remain open tend to have difficult proofs. "Difficult" nowadays often implies requiring computer assistance, as seen in both the proof of the Kepler conjecture and of the four-color theorem. Both proofs share similar ideas of "localizing": the local density redistribution in the Kepler conjecture proof and the discharging method in the proof of the four color theorem. Such problems lie at the edge of mathematics and computer science and to resolve them, one should combine theoretical tools and computer assistance. Both are essential: a strong theoretical basis must be built to make computer calculations feasible in terms of time and memory costs. The resulting proofs are a combination of mathematical arguments and code, whose correctness can hardly be verified by humans. This is where, for both of these results, computer verifications (proof assistance) comes into play.
The course is divided into three parts. The first part focuses on disc and sphere packings, notably the Kepler conjecture, and some open questions in the domain. The second part explores the history and the proof of the four-color theorem, as well as the exhaustive search of pentagonal tilings. The final part of the course is about proof verification, notably in the context of the Kepler conjecture and the four-color theorem. Interval arithmetic, a central tool used throughout the course, will be covered in the early lectures.
Daria Pchelina, Michael Rao, Damien Pous, Nathalie Revol