Proof-checking in ScienceNews
The current issue of ScienceNews has an interesting article on computer-assisted checking of mathematical proofs. The article explains the issue of how to verify that a proof is correct — an issue that has become increasingly important in mathematics, given the rise of extremely large proofs such as Andrew Wiles’ proof of Fermat’s Last Conjecture.
Proof-checking is something that we know a lot about here at CMU. Bob Harper, when he still a doctoral student at Cornell, worked on one of the seminal proof systems, NuPrl. Dana Scott and Bob Harper had connections to the groundbreaking Edinburgh LCF proof development system. And, of course, Frank Pfenning has done a huge amount of work in this area, particularly on the development and widespread use of his Twelf metalogical programming/proof system. Today, Bob Harper, Frank Pfenning, Karl Crary, and an army of undergraduate and graduate students do research and course homework assignments involving proofs that are checked automatically.
And yes, being a grader for one of these courses is a pretty sweet deal. ;-)
Peter Lee @ November 18, 2008
I should mention that proof-checking has also been a major part of my research career. The work on Proof-Carrying Code that George Necula and I did some years ago was completely dependent on the idea that it was practical to check proofs automatically.
This month’s Notices of the AMS is also entirely devoted to this topic (http://www.ams.org/notices/200811/). Local Thomas Hales’s article is particularly nice, I think.