Blog: Proof by Computer

Proof by Computer
EurekAlert (11/06/08)

New developments in the use of formal proof in mathematics are investigated by a series of articles by leading experts, published in the December 2008 edition of the Notices of the American Mathematical Society. The traditional method of proving theorems involves mathematicians presenting the argument in narrative form, and the correctness of the arguments is decided by the analysis of other mathematicians, in informal discussions, in lectures, or in journals. Problems of reliability inevitably crop up because the process of verifying mathematical results is basically social and therefore prone to error, and so the field of formal proof was developed to circumvent these shortcomings. A formal proof is one in which every single logical presumption has been checked all the way back to the basic mathematical precepts, and technology has advanced in recent years so that computer proof assistants that perform such checking are sufficiently powerful to accommodate challenging proofs. If the use of these assistants proliferates, the practice of mathematics could be dramatically revised. One vision is to have formal proofs of all central mathematical proofs, which Thomas Hales of the University of Pittsburgh compares to "the sequencing of the mathematical genome." The quartet of articles analyzes the current state of the art of formal proof and offers practical guidance for employing computer proof assistants.

View Full Article