Georges Gonthier (Microsoft Research): The Computer Mathematics of the Four Colour Theorem

The computer formalization of a theorem isn't just an exercise in verification; it can also provide new mathematical insight, that come from rigorously defining all key concepts. We will illustrate this thesis with examples drawn from our recent formalization of the proof of the Four Colour Theorem in Coq. The concept of planarity is central to this proof. Planarity has topological and combinatorial characterizations, which are often confused in arguments that are both pictorially appealing and logically incomplete. The rigor of our computer proof imposed a strict separation between the two. On the one hand we developed a purely combinatorial theory base on a symmetrical presentation of hypermaps, and to new results such as an elegant analogue of the Jordan Curve property. These led to several simplifications in the proof, in particular for constructing embeddings. On the other hand we realized that the Theorem could be proved under minimal topological assumptions; in particular our proof is independent of the Jordan Curve theorem, because we only use the Euler formula to move from topological to combinatorial planarity.