Verifying the Four Colour Theorem
| Georges Gonthier | Microsoft Research Cambridge |
Notice: At Stanford University NOT at SRI
Date: Friday May 27, 2005 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 in order to sign in and be escorted to the conference room. SRI is located at 333 Ravenswood Avenue in Menlo Park. Visitors may park in the visitors lot in front of Building E, and should follow the instructions by the lobby phone to be escorted to the meeting room. Detailed directions to SRI, as well as maps, are available from the Visiting AIC web page. 
©2013 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy |
