12
$\begingroup$

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?

Improve this question
$\endgroup$
3
  • $\begingroup$ 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. $\endgroup$
    – Kim Morrison
    Commented Nov 10, 2009 at 7:59
  • 4
    $\begingroup$ 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. $\endgroup$
    – Gil Kalai
    Commented Nov 10, 2009 at 12:19
  • $\begingroup$ 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. $\endgroup$
    – Anton Geraschenko
    Commented Nov 10, 2009 at 15:02

3 Answers 3

Reset to default
12
$\begingroup$

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.

Improve this answer
$\endgroup$
1
$\begingroup$

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).

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ These points are all patently false: Mizar is by all standards an archaic language that has been vastly improved upon, there are quite nice formalized theorem databases in most mature interactive theorem provers and proof automation is already quite sophisticated (but not as much as mathematicians would like, of course). $\endgroup$
    – cody
    Commented Mar 24, 2015 at 16:24
  • 1
    $\begingroup$ @cody - next time look at the date of what you are responding to (or down-voting) $\endgroup$
    – David Lehavi
    Commented Mar 27, 2015 at 10:26
  • 1
    $\begingroup$ I did look at the date! I believe that anything I'm saying was already true in 2010. See e.g. all this nice work. $\endgroup$
    – cody
    Commented Mar 27, 2015 at 13:35
1
$\begingroup$

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.

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged .