November 6, 2008, Providence, RI---New computer tools have thepotential to revolutionize the practice of mathematics by providingfar more-reliable proofs of mathematical results than have ever beenpossible in the history of humankind. These computer tools, based onthe notion of "formal proof", have in recent years been used toprovide nearly infallible proofs of many important results inmathematics. A ground-breaking collection of four articles by leadingexperts, published today in the Notices of the American MathematicalSociety (http://www.ams.org/notices), explores new developments in the use of formal proof in mathematics.
When mathematicians prove theorems in the traditional way, they present the argument in narrative form. They assume previous results, they gloss over details they think other experts will understand, they take shortcuts to make the presentation less tedious, they appeal to intuition, etc. The correctness of the arguments is determined by the scrutiny of other mathematicians, in informal discussions, in lectures, or in journals. It is sobering to realize that the means by which mathematical results are verified is essentially a socialprocess and is thus fallible. When it comes to central, well knownresults, the proofs are especially well checked and errors areeventually found. Nevertheless the history of mathematics has manystories about false results that went undetected for a long time. Inaddition, in some recent cases, important theorems have required suchlong and complicated proofs that very few people have the time,energy, and necessary background to check through them. And someproofs contain extensive computer code to, for example, check a lot ofcases that would be infeasible to check by hand. How canmathematicians be sure that such proofs are reliable?
To get around these problems, computer scientists and mathematiciansbegan to develop the field of formal proof. A formal proof is one inwhich every logical inference has been checked all the way back to thefundamental axioms of mathematics. Mathematicians do not usuallywrite formal proofs because such proofs are so long and cumbersomethat it would be impossible to have them checked by humanmathematicians. But now one can get "computer proof assistants" to dothe checking. In recent years, computer proof assistants have becomepowerful enough to handle difficult proofs.
Only in simple cases can one feed a statement to a computer proofassistant and expect it to hand over a proof. Rather, themathematician has to know how to prove the statement; the proof thenis greatly expanded into the special syntax of formal proof, withevery step spelled out, and it is this formal proof that the computerchecks. It is also possible to let computers loose to exploremathematics on their own, and in some cases they have come up withinteresting conjectures that went unnoticed by mathematicians. We maybe close to seeing how computers, rather than humans, would domathematics.
The four Notices articles explore the current state of the art offormal proof and provide practical guidance for using computer proofassistants. If the use of these assistants becomes widespread, theycould change deeply mathematics as it is currently practiced. Onelong-term dream is to have formal proofs of all of the centraltheorems in mathematics. Thomas Hales, one of the authors writing inthe Notices, says that such a collection of proofs would be akin to"the sequencing of the mathematical genome".
The four articles are:
- Formal Proof, by Thomas Hales, University of Pittsburgh
- Formal Proof---Theory and Practice, by John Harrison, Intel Corporation
- Formal proof---The Four Colour Theorem, by Georges Gonthier, Microsoft Research, Cambridge, England
- Formal Proof---Getting Started, by Freek Wiedijk, Radboud University, Nijmegen, Netherlands
The articles appear today in the December 2008 issue of the Noticesand are freely available at http://www.ams.org/notices.
Source: American Mathematical Society