Georges Gonthier, Microsoft Research
Verifying the Four Colour Theorem
Abstract
The 150-year-old Four Colour Theorem is the first famous result with a
proof that requires large computer calculations. Such proofs are still
controversial: It is thought that computer programs cannot be reviewed
with mathematical rigor. To overturn this belief, we have created a
fully computer-checked proof of the Four Colour Theorem. Using the Coq
proof assistant, we wrote an extended program that specifies both the
calculations and their mathematical justification. Only the interface
of the program - the statement of the theorem - needs to be
reviewed. The rest (99.8%) is self-checking: Coq verifies that it
strictly follows the rules of logic. Thus, our proof is more rigorous
than a traditional one.
Biography
Georges Gonthier received his Doctorate in 1988 from Université Paris
XI for work on the Esterel reactive programming language. After two
years at AT&T Bell Labs, he returned to France at INRIA in 1990. His
work includes the optimal computation of functional programs, the
formal verification of a concurrent memory management algorithm, and
concurrency analysis of the Ariane 5 flight software. Dr Gonthier
joined Microsoft Research Cambridge in 2003, where he completed the
first fully computer-checked proof of the famous Four Colour Theorem.