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

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.


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


Full Text: Link