I am going to answer the question as if you asked about massive *formalization of proofs*, not automatic extraction of formal proofs from existing informal proofs written in books, because that's a fairly hopeless task. One of the major lessons learned by Gonthier et al. was that published proofs rely on large amounts of implicit knowledge that is insufficiently recorded by current ways of writing mathematical texts.

**[Added 2015-07-07]** To address the comments, let me explain what the "missing knowledge" is. It is not about missing parts of a proof or missing details, we know how to deal with a lot of those through automation. Rather, the missing knowledge is more like what Andy Putman's comments suggested. For instance, the text might not explain the overall structure of the argument. Or, without telling, it just does a special case, and never explains why that is sufficient. Or, it forgets to mention that all vector spaces appearing in a given construction are actually subspaces of an ambient space, and therefore it makes sense to speak of their intersections and inclusions of one in another. These things are typically obvious to an experienced mathematician, but are *not written anywhere in the text*. And so they are hard for computers and graduate students to understand.

One of the major points of Gonthier et al. effort was to make sure that the formalization stayed very close to the actual text. The formalized proofs follow very closely the reasoning in the text, with as little extra details added in as possible. It was difficult to do this and it lead to several new techniques of formalization. Essentially, the proof assistants were adapted so that they could do the same sort of guesswork that a mathematician does when presented with insufficient information. Proof assistants have gotten much better at understanding what the user wants without having all the details spelled out for them.

People who promote formalization do *not* expect anyone to actually waste their time on boring details. *Of course* we want our proof assistants to be able to follow high-level arguments and fill in the details automatically, and so the community has worked hard to develop tools and techniques for doing this sort of thing, but much remains to be done. Dismissing the proof assistant as if by necessity they are clumsy tools that hinder mathematical ideas is like dismissing lasers because they require a roomful of equipment to function. In those areas where proof assistants actually work well, their users will tell you that *the first thing* they do when they want to try a new idea is to type it into a proof assistant. This for example has been my experience with the Twelf system which is designed for the purposes of formalizing formal systems (so a special-purpose tool).

Our experience with formalization of mathematics shows that formalization is possible, but with a lot of extra effort with available technology. It requires rethinking about how to organize mathematics so that it is amenable to formalization. For a moderately large formalization effort the issues arising are not mathematical but software-engineering: how to organize libraries so that they can be reused, what naming conventions to use, how to search existing libraries of theorems, etc.

Adoption of formalized mathematics is relatively slow because mathematicians have little reason to formalize their proofs. They can easily publish them unformalized, they feel that formalization just obscures matters (when in fact it forces one to really clean up after oneself), and that it is generally not worth doing. And so formalization is left to a few enthusiasts and computer scientists who need formal proofs in their work.

It is instructive to look at sub-communities that adopted formalization as a standard. In theoretical computer science this has happened in the programming language community. There many, many proofs proceed by consideration of a large number cases, of which only a couple are usually interesting. This is the perfect situation for proof assistants which can dispose of the boring stuff while making sure nothing is missed. The first ones to formalize their proofs were people who actually implemented the proof assistants. Then it was their students, the other people's students, and once the young people knew how to use the tools, the senior people joined the bandwagon (and many still prefer to use students). At any rate, in a conference on programming languages it has become the norm to say "and we formalized our proofs". To give you an idea where we are now: students who are just beginning their PhD's in this area often already are accomplished proof assistant hackers.

If we had to engineer massive adoption of formalization in mathematics, I would recommend two things:

- Better tools.
- Teach young people how to formalize mathematics.

There is a lot of room for improvement of the tools we use, and we can't teach old dogs new tricks.

Let me also explain why I think formalization is worth doing. It is *not* because we will know for sure that all that math is correct – it's irrelevant for most published math whether it is correct because the most important purpose of publication is academic promotion and not dissemination of ideas (cynical but true, just think why Elsevier is possible). The great potential of formalized mathematics is that it will give humans the ability to solve mathematical problems whose proofs are so complicated that no single human or small group of humans can comprehend or oversee using traditional methods. Another great promise is that formalized mathematics can be understood and used by machines. I guess I am looking forward to becoming the Borg.

6more comments