[FOM] formal proofs

[Jeremy Avigad]

Friends,

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
computer scientists:


http://cacm.acm.org/magazines/2014/4/173219-formally-verified-mathematics/fulltext

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

  http://www.andrew.cmu.edu/user/avigad/Talks/baltimore.pdf

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

  http://www.bourbaki.ens.fr/TEXTES/1086.pdf

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

  http://arxiv.org/abs/1302.2898

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

  http://www.ams.org/notices/200811/

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

  http://www.andrew.cmu.edu/user/avigad/Reviews/hales.pdf

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

  http://arxiv.org/abs/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.
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:

  http://arxiv.org/abs/1405.7012

The Feit-Thompson theorem:

  http://link.springer.com/chapter/10.1007%2F978-3-642-39634-2_14
  http://hal.inria.fr/hal-00816699

Homotopy limits, in the framework of homotopy type theory:

  http://arxiv.org/abs/1304.0680

The prime number theorem:

  http://dl.acm.org/authorize.cfm?key=929837

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 here:

  http://www.andrew.cmu.edu/user/avigad/Talks/clarke.pdf

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:

  http://link.springer.com/chapter/10.1007%2F978-3-319-08970-6_5
  http://arxiv.org/abs/1404.4410

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.

Best wishes,

Jeremy
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20141020/1f156a7c/attachment.html>