Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

I recently came across a concept of automated proof checking. I am very intrigued by the idea, that in the future all the proofs could be verified by a computer.

Moreover, some proofs were already verified. However, as I understand those proofs were formulated within the first-order logic.

In layman’s terms could somebody explain to the rest of the mathematicians: how complicated proofs can we verify already? What is the current progress on verifying major results, what are the challenges and possible approaches?

Thank you.

share|improve this question
    
The major challenge is developing libraries. According to [1], developing a library to formalize all of undergraduate mathematics will take more than a hundred man-years. [1] A F. Wiedijk. Estimating the Cost of a Standard Library for a Mathematical Proof Checker, 2002 PDF. –  user2468 Feb 25 '12 at 19:09
2  
@J.D. Actually, if that estimate turned out to be correct, that's not so bad and would be dwarfed by many successful software products currently in existence (think Word, Windows, etc). Specifically, it has been estimated that the Windows 7 development team for instance comprised over 1000 developers. –  ItsNotObvious Feb 25 '12 at 19:52
1  
@3Sphere True. But software enterprises such as Microsoft can make serious money out of large products such as Windows. This will not be the case with, say, a Coq library for proving Sylow theorems. –  user2468 Feb 25 '12 at 19:57
add comment

1 Answer 1

up vote 3 down vote accepted

The mechanics of verifying proofs by computer is pretty much a solved problem. We have a good solid understanding of what a valid proof step is and how to recognize its validity by machine.

What is holding up the entire enterprise is that even though we have a good theory of the structure of proofs, computers cannot understands English, so the proofs we want them to check need to be translated into the formal language that the proof checker works with. The result often looks more like program source code than mathematical prose. This translation is not yet quite routine, but not an impenetrable black art either.

A problem is that there is a very large body of background knowledge that is generally assumed already known by mathematicians working at the research frontier. Before the proof checkers can begin dealing with contemporary results, all of that has to be transcribed. And the transcribing has to be done by people with a quite solid understanding of logic and mathematics -- who could easier find more interesting things to use their time for.

For some time, it has been possible to earn a Ph.D. by grabbing a suitable chunk of undergraduate mathematics and formalizing that in a computer proof system. But the novelty of that is going to wear off and eventually stop impressing Ph.D. committees (this may already have happened, for all I know). And then motivating people to do the work is going to be a real problem. It is not high-profile enough that funding bodies are likely to pay anyone to do the drudgery, not for a sufficient amount of work.

I think the general hope is that the development of result libraries will eventually be done through some kind of crowdsourcing, like open-source software. But what kind of reward structure would make that work is still to be seen.

share|improve this answer
    
So everything within ZFC could theoretically be verified already? –  Tom Artiom Fiodorov Feb 25 '12 at 19:54
    
@ArtiomFiodorov: Yes, certainly. It's just a question of writing down the proofs in a format recognized by the verifier. –  Henning Makholm Feb 25 '12 at 19:56
    
@ArtiomFiodorov: I'm not very optimistic about that; natural language processing is its own can of worms entirely, and actual published proof prose often contains appeal to, say, geometric intuition, that somebody would have to formalize. The best one could hope for would be something like Google Translate which could produce a draft suggestion that would have to be corrected/extended by a human whenever the thing it comes up with doesn't verify (which, I imagine, would be quite often). –  Henning Makholm Feb 25 '12 at 20:36
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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