24
$\begingroup$

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.

Improve this question
$\endgroup$
10
  • 1
    $\begingroup$ I think this is a great topic of discussion, perhaps in a semester-long graduate course, and one that I am eager to hear answers to. I worry that it is too broad for MO, where there's a lot of emphasis placed on questions having a "correct" answer. But I hope to be mistaken. $\endgroup$
    – Theo Johnson-Freyd
    Commented Jul 6, 2015 at 2:28
  • 3
    $\begingroup$ Since you mention "Google Books style" as a goal (whatever that may mean), the present quality of Google Translate doesn't inspire much confidence for anytime soon. :) $\endgroup$
    – grghxy
    Commented Jul 6, 2015 at 4:56
  • 9
    $\begingroup$ Well, it's safe to say, the re-capchas are gonna be way more complicated... $\endgroup$
    – Per Alexandersson
    Commented Jul 6, 2015 at 6:48
  • 2
    $\begingroup$ The problem is really a composition of two problems: (1) How difficult is it to formalize real mathematical proofs for a person who perfectly understands the proof and the proof assistant?, and (2) How difficult is it for a computer to parse a proof written for humans, essentially guessing the missing steps and filling in the gaps left to the reader? Question (1) is about logic and programming paradigms (in particular, about our still imperfect understanding of constructivism and the tacit uses of univalence). Question (2) is an AI question (probably the simplest AI question, not that this ... $\endgroup$
    – darij grinberg
    Commented Jul 6, 2015 at 17:32
  • 4
    $\begingroup$ The problems in understanding mathematical English, even in formally written papers, is well described in the book The Language of mathe­matics, by Mohan Ganesalingam, and many other examples are given in my website athttp://www.abstractmath.org/MM/MMLangMath.htm $\endgroup$
    – SixWingedSeraph
    Commented Jul 7, 2015 at 13:22

3 Answers 3

Reset to default
23
$\begingroup$

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:

  1. Better tools.
  2. 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.

Improve this answer
$\endgroup$
12
  • 1
    $\begingroup$ I fear I find this somewhat inconcrete. In my limited experience with Coq, I have encountered some rather specific roadblocks, such as lack of documentation (even installation on Linux isn't something I can reliably do), a steep learning curve, and annoyances such as the fact that every other set I need is really a setoid and I'd have to learn a whole new yoga to work with them (without really having much pre-existing knowledge to learn from, since everyone else seems to either avoid the need for setoids or assume univalence to get rid of it). I think there are far more people who are ... $\endgroup$
    – darij grinberg
    Commented Jul 6, 2015 at 17:41
  • 4
    $\begingroup$ I think that the words "implicit knowledge" might be misleading. It's not that there are folklore theorems that people are using. Rather, there are lots of routine arguments that people have seen over and over again during their education. When you write a paper, you don't spell these out, but just give the major steps. Experts can easily see what is going on. Students suffer a bit; this is why graduate students often spend days on single pages of papers. I should say that this is true even for good writing. If you give too many details, it can be hard to sort out where the "meat" $\endgroup$
    – Andy Putman
    Commented Jul 6, 2015 at 18:22
  • 3
    $\begingroup$ of the argument is. I've gotten annoyed at papers plenty of times for giving too many routine details. But proof assistants can't fill in the missing parts by themselves. You have to spend way too much time on the boring stuff. That's why I for instance am not interested in spending time trying to formalize my proofs. $\endgroup$
    – Andy Putman
    Commented Jul 6, 2015 at 18:23
  • 2
    $\begingroup$ I feel like there must be a diagonalization argument showing that there cannot be an algorithm to reduce all "routine" arguments. $\endgroup$
    – Alexander Woo
    Commented Jul 6, 2015 at 19:30
  • 5
    $\begingroup$ I have asked people from Gonthier's team to write an answer. Let's hear it from the horse's mouth. $\endgroup$
    – Andrej Bauer
    Commented Jul 7, 2015 at 14:59
22
$\begingroup$

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.

Improve this answer
$\endgroup$
5
  • $\begingroup$ Thanks for the insider view! Do you know if there is a beginner-friendly introduction into the use of these libraries these days? I must admit I am glad to hear that the "cryptic boilerplate code" appears cryptic even to its authors and not just to me; but I would be really happy to be able to understand at least the non-too-technical parts of it. Is there something that is less fast-paced than the 2009 "tutorial" (also newer -- two of its examples don't compile anymore) and less technical than the Manual? $\endgroup$
    – darij grinberg
    Commented Jul 11, 2015 at 18:12
  • $\begingroup$ Interesting: your answer made me realize I forgot the "seemingly" in my answer (now edited). For the time being, only a few tutorial-like references are available: An introduction to small scale reflection in Coq A.M. and G. Gonthier (2010, a bit outdated too); the material of a 2012 summer school; a recent course by Ilya Sergey, for a computer-oriented audience. $\endgroup$
    – Assia Mahboubi
    Commented Jul 12, 2015 at 9:25
  • $\begingroup$ The 2010 tutorial is rather nice, though I still cannot compile its Lemma edivnP. The "rewrite -{1}(subnK le_dm) -addSn addnA -mulSnr" instruction breaks, maybe because mulSnr has changed its statement, or rewrite has changed its behavior. I have tried reading Sergey but he was too terse for me at the important points... $\endgroup$
    – darij grinberg
    Commented Jul 12, 2015 at 10:13
  • 1
    $\begingroup$ You're right, the 2010 tutorial is outdated (at least for the Coq scripts), sorry about that. We're now trying to write an updated and more comprehensive document. But it will probably take an other few months to reach a readable state. Thus we should probably also try to maintain the old version alive meanwhile... $\endgroup$
    – Assia Mahboubi
    Commented Jul 12, 2015 at 14:07
  • $\begingroup$ "We're now trying to write an updated and more comprehensive document." That's wonderful news, thank you! $\endgroup$
    – darij grinberg
    Commented Jul 12, 2015 at 14:18
5
$\begingroup$

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.

Improve this answer
$\endgroup$

You must log in to answer this question.

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