Proof by Computer Gaining Traction

November 11, 2008

New computer tools, based on the notion of formal proof, have the potential to revolutionize the practice of mathematics. Such computer-based formulations of the lengthiest, most difficult, and most complex ideas, statements, and theorems in mathematics reduce the drudgery of producing rigorous proofs and substantially increase their reliability.

Four articles, published in December 2008 issue of the Notices of the American Mathematical Society,  (www.ams.org/notices), explore the growing use of formal proofs and "computer proof assistants" in mathematics. The articles examine the state of the art of formal proofs and offer guidance for using computer-based tools to formulate proofs.

A significant move to formal proofs, the articles reveal, would alter mathematical practices: Computers, rather than people, would do the most laborious and time-consuming work. Machines, moreover, might discover new mathematics. And there could even be more time for mathematicans to teach.

One long-term result would be formal proofs of the central theorems in mathematics. Such a collection of proofs would be akin to "sequencing of the mathematical genome," Thomas Hales of the University of Pittsburgh) noted.

The articles are: "Formal Proof," by Thomas Hales; "Formal Proof—Theory and Practice," by John Harrison; "Formal Proof—The Four-Color Theorem," by Georges Gonthier; and "Formal Proof—Getting Started," by Freek Wiedijk.

Source: American Mathematical Society, Nov. 6, 2008.