Proof Formalization in Mathematics: Guest Post by Jeremy Avigad

There’s a discussion going on at the Foundations of Mathematics mailing list about the purpose and value, actual and potential, for formalized proofs in mathematics.  Harvey Friedman asked Jeremy Avigad to comment; he sent this super-useful list of references, republished here with his approval.

John Harrison and I recently wrote a survey on formalized mathematics, for computer scientists:

Here are some slides from a related talk that I presented at the AMS Joint Meetings in Baltimore earlier this year:

Tom Hales recently wrote a nice piece for the Bourbaki seminar:

He has another lovely survey here (which discusses computation in mathematics more generally):

There is an issue of the Notices of the AMS from 2008 dedicated to formal proof:

I recently wrote a review of Hales’ nice book on the proof of the Kepler conjecture, to appear in the Bulletin of Symbolic Logic:

Here is a survey of mine on some of the difficulties involved in making sense of ordinary mathematical language and notation:

There is now a substantial literature on formal mathematics, and writeups of formalizations regularly appear in conferences like Interactive Theorem Proving (ITP), as well as journals like the Journal of Automated Reasoning. Homotopy type theory has also gotten a lot of press lately, in parts for its interest as a new framework for verification.

Here are some formalizations I personally have worked on:

Most of these have something to say about the current challenges and difficulties.

There are number of good interactive theorem provers out there. I am currently involved in the design and library development for a new one, Lean, being developed by Leonardo de Moura at Microsoft (it is an open source project): 

https://github.com/leanprover/lean

There are slides describing it.  It is in its early stages, and not yet fully functional, but I am excited about it. We are aiming for a public “release” early next year.

As indicated in many of the publications just listed, progress is needed before interactive theorem provers are commonly used, though I am absolutely certain it will eventually happen. This includes things like developing better user interfaces, automated support, and libraries. A student of mine, Rob Lewis, and I are working on a heuristic method of proving real-valued inequalities, described here:

Jeremy Avigad, Robert Y. Lewis, Cody Roux, 2013, “A heuristic prover for real inequalities,” arXiv:1404.4410 and LNCS 8558 (2014)

Many others are developing other types of automation, both for the purposes of supporting the verification of mathematical proof, and for supporting the verification of hardware and software.

I apologize for over-emphasizing my own projects; there is a tremendous amount of work being done in the area of now, and mine is just a small part of it. I once heard Natarjan Shankar say that this is “the golden age of metamathematics,” and I agree.  This is a really exciting time to be working with formal methods.

Leave a Reply

Your email address will not be published. Required fields are marked *