Woensdag 6 april 2005
Spreker: 
Georges Gonthier (Microsoft Research Cambridge)

Titel: 
Verifying the Four Colour Theorem

Tijd: 
11:00  12:00

Plaats: 
CK N4 (N3045)

Vanaf kwart voor 11 is er koffie en chocola in de Weylkamer
(N2046).
Abstract
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
computerchecked 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 selfchecking: 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 pencilandpaper
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. We largely use software engineering techniques to
develop this proof. In addition to making the whole project feasible,
this approach also yielded new insights into the mathematics of the
problem.