University of Calgary

Four Color Theorem Verified in Coq

This website has moved!

You are looking at an archived page. The website has moved to richardzach.org.

Submitted by Richard Zach on Thu, 04/21/2005 - 4:43pm

Georges Gonthier (MS Research, Cambridge) has a paper up entitled "A computer-checked proof of the Four Colour Theorem." The original proof of the theorem by Appel and Haken relied on computer programs checking a very large number of cases, and raised some important conceptual and philosophical issues (see Tymoczko, "The four-color theorem and its philosophical significance," Journal of Philosophy 76 (1979) 57-83 and reprinted in his collection New Directions in the Philosophy of Mathematics). The new work has formalized a more recent version of the proof and verified it in the proof checker Coq. Here's how Gonthier describes the contribution this is making:

Our work can be seen as an ultimate step in this clarification effort, completely removing the two weakest links of the proof: the manual verification of combinatorial arguments, and the manual verification that custom computer programs correctly fill in parts of those arguments. To achieve this, we have written a formal proof script that covers both the mathematical and computational parts of the proof. We have run this script through the Coq proof checking system [13,9], which mechanically verified its correctness in all respects. Hence, even though the correctness of our proof still depends on the correct operation of several computer hardware and software components (the processor, its operating system, the Coq proof checker, and the Ocaml compiler that compiled it), none of these components are specific to the proof of the Four Colour Theorem. All of them come off-the-shelf, fulfill a more general purpose, and can be (and are) tested extensively on numerous other jobs, probably much more than the mind of an individual mathematician reviewing a proof manuscript could ever be. In addition, the most specific component we use the Coq system, to which the script is tuned can output a proof witness, i.e., a longhand detailed description of the chain of formal logical steps that was used in the proof. This witness can, in principle, be checked independently (technically, it is a term in a higher-order lambda calculus). Because this witness records only logical steps, and not computation steps, its size remains reasonable, despite the large amount of computation needed for actually checking the proof.

Formalizing and verifying theorems (by computer) seems to be a hot topic, and might raise interesting questions for the philosophy of mathematics; see Jeremy Avigad's work on formalizing mathematics in Isabelle.

(Via Lambda the Ultimate)