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:
- Jeremy Avigad, John Harrison, 2014, “Formally verified mathematics.” Communications of the ACM 57: 66-75
Here are some slides from a related talk that I presented at the AMS Joint Meetings in Baltimore earlier this year:
- Jeremy Avigad, 2014, “Formal verication, interactive theorem proving, and automated reasoning“
Tom Hales recently wrote a nice piece for the Bourbaki seminar:
- Thomas C. Hales, 2013-14, “Developments in formal proofs“, Séminaire Bourbaki 1086
He has another lovely survey here (which discusses computation in mathematics more generally):
- Thomas C. Hales, 2013, “Mathematics in the age of the Turing machine,” arXiv:1302.2898
There is an issue of the Notices of the AMS from 2008 dedicated to formal proof:
- Special Issue on Formal Proof, with contributions by Tom Hales, Georges Gauthier, John Harrison, and Freek Wiedijk
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:
- Jeremy Avigad, 2012, “Type inference in mathematics,” arXiv:1111.5885
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:
- The central limit theorem
- The Feit-Thompson theorem
- Homotopy limits, in the framework of homotopy type theory:
- The prime number theorem
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.