State of the progess of the automated proof checking

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.

• 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
Commented Feb 25, 2012 at 19:09
• @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. Commented Feb 25, 2012 at 19:52
• @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
Commented Feb 25, 2012 at 19:57

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.

• So everything within ZFC could theoretically be verified already? Commented Feb 25, 2012 at 19:54
• @ArtiomFiodorov: Yes, certainly. It's just a question of writing down the proofs in a format recognized by the verifier. Commented Feb 25, 2012 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). Commented Feb 25, 2012 at 20:36
• @TomArtiomFiodorov: I once had to prove the infinite Ramsey theorem in Coq (one of this proof-checking softwares). While the (mathematical) proof of this theorem is pretty straightforward, it turned out that the Coq proof was 750+ lines long, most of it being silly stuff about induction and sequences. Commented May 15, 2015 at 15:54

Some complicated proofs have been verified by computer, the well known example in mathematics are:

• the 4-colors theorem by Georges Gonthier and Benjamin Werner.

• the Feit-Thompson theorem by Gy Georges Gonthier and its team.

• the Kepler conjecture (Tomas Hales' theorem) by the flyspeck team.

There are other examples in Computer Science:

• a C compiler: CompCert by Xavier Leroy

• the functional correctness of a general-purpose operating system kernel by NICTA

As Henning explained the proof theory has already been well explored and it is quite clear how to check a formal proof.

But there are still many challenges:

• how to exchange proofs between different systems

• how to edit proof and check proof in wikipedia like environment

• what is the best way to formalize some given concept

• how to modify the proof assistant to allow a language closer to the usual mathematical language: overloaded notations, implicit steps in the proof, implicit coercions, how to deal with proofs by analogy or symmetry, ...

• how to mix efficient computations and proofs

• how to automate proofs

• ...