Computers checking mathematical proofs?
Computer-assisted of mathematical proofs are not new. For example, computers were used to confirm the so-called 'four color theorem.' In a short release, 'Proof by computer,' the American Mathematical Society (AMS) reports it has published a special issue of one its journals dedicated to computer-aided proofs. 'The four Notices articles explore the current state of the art of formal proof and provide practical guidance for using computer proof assistants.' And as said one of the researchers involved, 'such a collection of proofs would be akin to the sequencing of the mathematical genome.' But read more...
Let's first look at how mathematical theorems were proven in the past. "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 social process and is thus fallible."
This is why the concept of 'formal proof' is now being used. "To get around these problems, computer scientists and mathematicians began to develop the field of formal proof. A formal proof is one in which every logical inference has been checked all the way back to the fundamental axioms of mathematics. Mathematicians do not usually write formal proofs because such proofs are so long and cumbersome that it would be impossible to have them checked by human mathematicians. But now one can get 'computer proof assistants' to do the checking. In recent years, computer proof assistants have become powerful enough to handle difficult proofs."
Here is a link to this special issue of the Notices of the American Mathematical Society (December 2008, Volume 55, Issue 11).
The first article is Formal Proof, by Thomas Hales of the University of Pittsburgh (PDF format, 12 pages, 512 KB). Here is the first paragraph. "Daily, we confront the errors of computers. They crash, hang, succumb to viruses, run buggy software, and harbor spyware. Our tabloids report bizarre computer glitches: the library patron who is fined US$40 trillion for an overdue book, because a barcode is scanned as the size of the fine; or the dentist in San Diego who was delivered over 16,000 tax forms to his doorstep when he abbreviated 'suite' in his address as 'su'." Hales adds that "on average, a programmer introduces 1.5 bugs per line while typing." As I wrote -- pretty good -- software for supercomputers for many years, I think Hales claim is a little exaggerated.
The second article is from Georges Gonthier, from Microsoft Research, in Cambridge, England, and is called Formal proof -- The Four Colour Theorem (PDF format, 12 pages, 2.58 MB). In addition to this highly technical paper, here are three links to Wikipedia articles about mathematical proofs, computer-assisted proofs and the four color theorem.
The third article has been written by John Harrison, who works for Intel Corporation. Here is a link to Formal Proof -- Theory and Practice (PDF format, 12 pages, 151 KB).
Here is the first paragraph. "A formal proof is a proof written in a precise artificial language that admits only a fixed repertoire of stylized steps. This formal language is usually designed so that there is a purely mechanical process by which the correctness of a proof in the language can be verified. Nowadays, there are numerous computer programs known as proof assistants that can check, or even partially construct, formal proofs written in their preferred proof language. These can be considered as practical, computer-based realizations of the traditional systems of formal symbolic logic and set theory proposed as foundations for mathematics."
The fourth article of this special Notices issue is called Formal Proof -- Getting Started, by Freek Wiedijk from Radboud University, Nijmegen, Netherlands (PDF format, 7 pages, 153 KB).
If you're a mathematician or a computer scientist, these four articles are must-read ones.
Sources: American Mathematical Society news release, November 6, 2008; and various websites
You'll find related stories by following the links below.