November 8th, 2008
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).
No comments:
Post a Comment