Search |  Contact |  SRI Home Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap. Do not follow this link, or your host will be blocked from this site. This is a spider trap.A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A A ASRI International.  333 Ravenswood Avenue.  Menlo Park, CA 94025-3493. SRI International is a nonprofit corporation.

AIC Seminar Series

Verifying the Four Colour Theorem

Georges GonthierMicrosoft Research Cambridge

Notice:  At Stanford University NOT at SRI

Date:  2005-05-27 at 13:00

Location:  History Bldg. 200 - Room 002  (Directions)

   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 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.

   Note for Visitors to SRI

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.

SRI International
©2014 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy