Formal proof - the four color theorem. (English) Zbl 1195.05026

Gonthier, Georges

Notices Am. Math. Soc. 55, No. 11, 1382-1393 (2008).

A critical examination of the 1976 and 1995 proofs of the four-color theorem leads to the conclusion that “both proofs combined a textual argument, which could reasonably be checked by inspection, with computer code that could not”. How might one realize formal program proofs? How might one write code that describes not only what the machine should do, but also why it should be doing it – a formal proof of correctness? The author of this article has been engaged for ten years in the attempt to produce such a proof for part of code from the 1997 proof by Robertson-Sanders-Seymour-Thomas. The successful answer led to a new question: Was the statement of the correctness proof itself correct? The answer to this question required the formalization of the entire proof of the four-color theorem, not just of its code. This aim was achieved in 2005. In this paper, after giving the background material, the author describes the mathematics involved in the formalization, stressing the fact that the problem considered is apparently not only one of topology and analysis: it is essentially a problem in combinatorics. The whole approach represents a remarkable contribution toward a deeper understanding of the nature of formal proofs.

Reviewer: Solomon Marcus (Bucureşti) (MR 2009j:05079)

MSC:

05C15	Coloring of graphs and hypergraphs
68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)

Citations:

Zbl 0377.94038; Zbl 0331.05106; Zbl 0681.05027; Zbl 1069.68095; JFM 44.0568.01; Zbl 0654.03045; Zbl 0313.05115; Zbl 1188.68002; Zbl 0187.20904; Zbl 0883.05056; Zbl 0505.05003; JFM 12.0409.01; Zbl 0308.05105; Zbl 0429.05006; Zbl 1030.05041

Software:

Coq