KnowledgeBase » SEMINAR » ID = 627

Verifying the Four Colour Theorem

by Georges Gonthier
2004-2005

The 150 year old Four Colour Theorem is famous for being the first important mathematical result whose proof, completed in 1976 by Appel and Haken, required computer calculations too large to be checked by hand. The controversy over such proofs has gone on ever since, fuelled by the belief that the reliability of the software performing these calculations could not stand up to mathematical standards. To put an end to this belief, we have just completed a fully computer-checked proof of the Four Colour Theorem. Using the Coq proof assistant technology developed at Inria, we wrote an extended program that specifies both the calculations required by the proof and their mathematical justification. Only the interface of the program a formal statement of the theorem needs to be reviewed for correctness. The rest (99.8%) is essentially self-checking: the Coq runtime automatically verifies that the mathematical parts strictly follow the rules of logic. Thus, this sort of program is more reliable than a pencil-and-paper proof. Though proof assistants have been around for some 30 years, we are the first to use them to prove a major result that absolutely requires the use of computers. The main technique we used to accomplish this, known as computation reflection, basically amounts to replacing mathematical proof with software debugging; this raises the perspective that proof assistant technology could be effectively transferred to the engineering of reliable and interoperable software.