[FOM] formal proofs
avigad at cmu.edu
Mon Oct 20 08:55:54 EDT 2014
Harvey asked me to comment on this thread, but I don't think I have
anything intelligent to say beyond things I have already said in print. So,
instead, I'll provide some references that may be helpful.
John Harrison and I recently wrote a survey on formalized mathematics, for
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
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.
As FOM readers know, homotopy type theory has also gotten a lot of press
lately, in parts for its interest as a new framework for verification (and
no, I don't want to reopen that discussion).
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
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
There are slides describing it here:
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:
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
mathematics," and I agree. This is a really exciting time to be working
with formal methods.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the FOM