Logblog: Richard Zach's Logic Blog

University of Calgary

UofC Navigation

You are looking at an archived page. The website has moved to richardzach.org.

Submitted by Richard Zach on Mon, 10/20/2014 - 6:34pm

*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.

- Richard Zach's blog
- Log in to post comments

- Open Logic Project
- The LogBlog is Moving!
- Academic Genealogy Graphed
- CfP: Hilbert’s Epsilon and Tau in Logic, Informatics and Linguistics
- In Memoriam: Grigori Mints
- Previously Unknown Turing Manuscript Going to Auction
- Carnap (and Goodman and Quine) and Linguistics (Guest post by Darin Flynn)
- Carnap on "Syntax" vs "Semantics"