Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Formalizing mathematical proofs so that they can be checked for correctness and manipulated by computer is a recurrent proposal, most notably stated in the QED manifesto (1994). The December 2008 issue of Notices of the AMS is entirely devoted to the state of the art in formal proof; an informal, general interest overview is provided by Cameron Freer's website vdash.org.

As practicing mathematicians, what's your perception of formal proof and interactive proof assistants? Are you familiar with current systems? Should they be used in mathematical education?

What are the obstacles to formal proof becoming a generally used tool, besides the effort required to build a useful library of current mathematical knowledge?

share|improve this question

closed as not a real question by Scott Morrison Nov 10 '09 at 7:58

It's difficult to tell what is being asked here. This question is ambiguous, vague, incomplete, overly broad, or rhetorical and cannot be reasonably answered in its current form. For help clarifying this question so that it can be reopened, visit the help center.If this question can be reworded to fit the rules in the help center, please edit the question.

    
Another question for the community wiki, methinks. –  Harald Hanche-Olsen Nov 9 '09 at 19:30
    
This seems to be a question without a definitive answer, and in particular requires discussion. As such, it's not appropriate at MO, per the FAQ. I'm actually not certain I'm following consensus to close here, so I've also flagged for other moderators to consider. –  Scott Morrison Nov 10 '09 at 7:59
3  
This is a fairly interesting question. There are many questions with no definite answers (like what is the most harmful heuristic) and I do not see the reason to close it. –  Gil Kalai Nov 10 '09 at 12:19
    
I agree with Scott closing this question. It's a very interesting question, but it's a discussion question, not a question that has a definite answer. As an artifact of being really good for very focused to-the-point questions, MO is really bad for discussions. Discussions should really happen on a blog or a threaded discussion forum, not MO, where the answers get rearranged and the comments are limited to 600 characters. See tea.mathoverflow.net/discussion/21#Item_3 for more of my thoughts. If you have some thoughts on this, please post on that meta.MO thread. –  Anton Geraschenko Nov 10 '09 at 15:02

3 Answers 3

Carlos Simpson, in the nineties wrote "Descente pour les n-champs" together with Andre Hirschowitz. Apparently they were quite ahead of their time: No one could be found to referee their paper. So to know whether it is correct or not, Simpson started developing an automatic theorem-checking program for category theoretical statements. Later it turned out that there was a small inaccuracy (they used covers where they needed hypercovers), but I don't know if it was found by help of the program... Anyway it clearly shows how it can be useful.

share|improve this answer

I'm not sure the question is real an MO question, but I'll bite; the three greatest obstacles are:

  • a theorems database (that's the easiest one)

  • a reasonable algorithm which can bridge trivial steps (they are trying to build one for years)

  • a reasonable language (the closest you have is Mizar, and it's very far from the way we write math)

In the current state of afairs, I don't think they are usefull even as proof verifiers, let alone proof assistants (I'm not refering to CASs - but to auto-proof verifiers).

share|improve this answer

I think that this is being used to verify results notably the Kepler conjecture by the Flyspeck project. So this is now one way to try to prove theorems and thus is of interest to practicing mathematicians.

share|improve this answer

Not the answer you're looking for? Browse other questions tagged or ask your own question.