AIC Seminar Series
Verifying the Four Colour Theorem
|Georges Gonthier||Microsoft Research Cambridge|
Notice: At Stanford University NOT at SRI
Date: 2005-05-27 at 13:00
Location: History Bldg. 200 - Room 002 (Directions)
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.
Please arrive at least 10 minutes early as you will need to sign in by
following instructions by the lobby phone at Building E. SRI is located
at 333 Ravenswood Avenue in Menlo Park. Visitors may park in the parking
lots off Fourth Street. Detailed directions to SRI, as well as maps, are
available from the Visiting AIC web page.
There are two entrances to SRI International located on Ravenswood Ave.
Please check the Builing E entrance signage.
©2014 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493