What technical and/or theoretical challenges are involved in automatically extracting proofs from books and papers into Coq code? Over the years, advances in machine learning has allowed us to communicate and interact, using the same natural language, more and more semantically with computers, e.g. Google, Siri, Watson, etc. On the other side, proof automation and formalization has gained more and more steam, culminating at, for example, recent efforts by Gonthier et al. to encode the Feit-Thompson theorem, and this trend will not stop as homotopy type theory has become a hot research topic. It then only seems natural to ask what open problems or technical challenges still lie ahead before we arrive at a Google Books style of automatically extracting human proofs written on paper (or just in latex) to formalized and checked proofs in something like Coq?
Ideally, answers regarding both the mathematical side and the more empirical machine learning side (or perhaps other viewpoints I've not considered here) are welcome, but I'm not quite sure if the latter is on topic on mathoverflow. And ideally, I should think we want to avoid babbling philosophy here, e.g. what's the point of mathematics, etc.
 A: There's a really nice survey article on this subject by Jeremy Avigad and John Harrison (both have had concrete experience in carrying out such formalizations "by hand"): Formally Verified Mathematics.
A: 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.
A: I think Andrej's opinion is very accurate. Here are a few more comments based on my experience as a contributor to the Coq proof of the Feit-Thompson theorem (sorry it's a bit long).
This formal development comprises three natures of libraries: some are for infrastructure purposes and no
mathematician cares about the lemmas they prove (litanies of lemmas on
booleans, lists or natural numbers, seemingly cryptic boilerplate code...),
some contain constructions (permutation groups, rational numbers,...),
and some contain meaningful theories (finite
group theory, linear algebra, character theory,...). At least in this
last category, which is by far the largest in size, the length of both
statements and proof scripts are of the same order of size than the
LaTeX code of their paper counterpart. The statements are kept as
readable as possible by a choice of LaTeX-like notations which mimic
the corresponding type-setting source
code. Proof scripts on the other hand look rather different, but long
ones (for long proofs) are usually structured with many explicitly
stated intermediate lemmas, that are as readable as the main one.
Beside a (dumb and merciless) proof checker, interactive proof
assistants actually include
various tools that are there to help with the gap issue.
As already mentioned in this thread, comprehensive and well-organized
libraries of formalized mathematics are a mandatory ingredient. Also
it is possible to automate the description of computational parts in proofs
by implementing formal-proof-producing decision or normalization
procedures (like for instance computer-algebra-like routines for
algebraic expressions). But this is not enough --and by the way the
libraries of the Feit-Thompson theorem actually barely use this latter
form of automation.
One crucial point there was to be able to input mathematical
sentences, for
instance the formal statement of wannabe theorems, with as much
facilities as one would write them on paper. Otherwise very soon you
just cannot read them (nor are you able to input them in fact).
But in that case you need to have the proof
assistant automatically and silently decorate the objects with the
implicit information carried by the standard mathematical notations.
Once the appropriate infrastructure is set (which requires
in particular understanding the common notational practices of the
authors in the field), the routine arguments mentioned by Andy Putman
require close to zero input from the user. For instance if you know
that $K$ and $H$ are two subgroups of a same group, showing that
$0 \lt \#(H \cap N(K))$ is just trivial (i.e. a two character Coq proof
script), because the system knows that the
normalizer of a group and the intersection of two
groups are themselves groups, and that the cardinal of a group is always
positive for a group has at least one (neutral) element. Indeed,
these bureaucratic steps can be implemented by a program chaining some
identified lemmas for you behind the scene. This either closes some
branches in the proof or calculates the glue needed to make your
current goal match the known result you want to use at this stage.
Crafting this infrastructure was one of the fun and creative parts of
the formalization work (it is not just about tagging some lemmas) and
I do not really see how automated tools could significantly help
here. There is still much to be done: we do not have yet, in any proof
assistant on the market, a comprehensive set of compatible formal
mathematical libraries that would encompass a common socle of theories
for graduate level in algebra and geometry and analysis etc.
For instance the libraries we wrote do not address real and complex
analysis at all. Although I am near to ignorant in AI or machine learning,
this seems to me a prerequisite step to have automated tools produce
formal proofs from any kind (script, paper, voice,...) of input description.
Yet the advent of modern ways of interacting with proof assistants (to
describe formal proofs, and search existing content) is probably
one of the major challenges to overcome, in order for proof assistants
to become as popular as computer algebra systems (or even type-setting
environments) among researchers in mathematics.
