Transcription of Formal Proof—The Four- Color Theorem
{{id}} {{{paragraph}}}
Example: air traffic controller
Formal Proof—The Four- Color Theorem
Formal Proof The Four- Color TheoremGeorges GonthierThe Tale of a BrainteaserFrancis Guthrie certainly did it, when he coined hisinnocent little coloring puzzle in 1852. He man-aged to embarrass successively his mathematicianbrother, his brother s professor, Augustus de Mor-gan, and all of de Morgan s visitors, who couldn tsolve it; the Royal Society, who only realized tenyears later that Alfred Kempe s 1879 solution waswrong; and the three following generations ofmathematicians who couldn t fix it [19].Even Appel and Haken s 1976 triumph [2] had ahint of defeat: they d had a computer do the prooffor them! Perhaps the mathematical controversyaround the proof died down with their book [3]and with the elegant 1995 revision [13] by Robert-son, Saunders, Seymour, and Thomas. Howeversomething was still amiss: both proofs combineda textual argument, which could reasonably bechecked by inspection, with computer code thatcould not.
that formal proofs are very difficult to produce, Georges Gonthier is a senior researcher at Microsoft Research Cambridge. His email address is gonthier@ microsoft.com. even with a language rich enough to express all mathematics. In 2000 we tried to produce such a proof for part of code from [13], just to evaluate how the field had progressed.
Loading..
Tags:
Information
Domain:
Source:
Link to this page:
Please notify us if you found a problem with this document: