Four Color Theorem Verified in Coq

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)

UPDATE: More links here and see also Brian’s post.

3 thoughts on “Four Color Theorem Verified in Coq

  1. Gonthier work on the verification of the correctness of the existing computer aided proof of the four color theorem is an remarkable result. But we should not give up and rely completely on the verification of theorems by computers. As an example, last year in August I have announced a non-computer proof of the four color theorem (Spiral Chains: A New Proof of the Four Color Theorem, http://arxiv.org/abs/math.CO/0408247/) which is based on a new concept called spiral chains. Although my proof has not been verified formally (not in the sense of a computer program but rather group of expert graph theorist) but no one yet be abled to provide an counter-example. Cahit Posted by I. Cahit

  2. My site has a simple proof of the four color conjecturefor the masses who want an explanation that is not soabstract. Any comments pro or con are welcome. Posted by r. hudson

  3. My site has a simple proof of the four color conjecturefor the masses who want an explanation that is not soabstract. Any comments pro or con are welcome. Posted by r. hudson

Leave a Reply

Your email address will not be published. Required fields are marked *