University of Calgary
UofC Navigation

Richard-Zach's blog

Proof Formalization in Mathematics: Guest Post by Jeremy Avigad

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:

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.

Awodey's "HoTT for Philosophers" on mathtube.org

Submitted by Richard-Zach on Fri, 10/17/2014 - 9:04am

Steve Awodey's talk in the Calgary Mathematics & Philosophy lecture series ("Univalence as a New Principle of Logic" aka "HoTT for Philosophers") is now up on mathtube.org.

bpextra: new version v 0.2

Submitted by Richard-Zach on Thu, 10/16/2014 - 9:22pm

I've fixed a bug in bpextra.The new version can be downloaded from github.

See also this issue for how to define your own deduction styles.

SotFoM II: Competing Foundations

Submitted by Richard-Zach on Thu, 10/16/2014 - 2:49pm

The second installment of SotFom (Symposium on the Foundations of Math) is asking for papers by Halloween:

http://sotfom.wordpress.com/2014/10/14/final-cfp-and-extended-deadline-s...

FINAL CFP and *EXTENDED DEADLINE*: SoTFoM II `Competing Foundations?’, 12-13 January 2015, London.

The focus of this conference is on different approaches to the foundations of mathematics. The interaction between set-theoretic and category-theoretic foundations has had significant philosophical impact, and represents a shift in attitudes towards the philosophy of mathematics. This conference will bring together leading scholars in these areas to showcase contemporary philosophical research on different approaches to the foundations of mathematics. To accomplish this, the conference has the following general aims and objectives. First, to bring to a wider philosophical audience the different approaches that one can take to the foundations of mathematics. Second, to elucidate the pressing issues of meaning and truth that turn on these different approaches. And third, to address philosophical questions concerning the need for a foundation of mathematics, and whether or not either of these approaches can provide the necessary foundation.

Date and Venue: 12-13 January 2015 – Birkbeck College, University of London.

Confirmed Speakers: Sy David Friedman (Kurt Goedel Research Center, Vienna), Victoria Gitman (CUNY), James Ladyman (Bristol), Toby Meadows (Aberdeen).

Call for Papers: We welcome submissions from scholars (in particular, young scholars, i.e. early career researchers or post-graduate students) on any area of the foundations of mathematics (broadly construed). While we welcome submissions from all areas concerned with foundations, particularly desired are submissions that address the role of and compare different foundational approaches. Applicants should prepare an extended abstract (maximum 1,500 words) for blind review, and send it to sotfom [at] gmail [dot] com, with subject `SOTFOM II Submission’.

Submission Deadline: 31 October 2014

Notification of Acceptance: Late November 2014

Scientific Committee: Philip Welch (University of Bristol), Sy-David Friedman (Kurt Goedel Research Center), Ian Rumfitt (University of Birmigham), Carolin Antos-Kuby (Kurt Goedel Research Center), John Wigglesworth (London School of Economics), Claudio Ternullo (Kurt Goedel Research Center), Neil Barton (Birkbeck College), Chris Scambler (Birkbeck College), Jonathan Payne (Institute of Philosophy), Andrea Sereni (Universita  Vita-Salute S. Raffaele), Giorgio Venturi (CLE, Universidade Estadual de Campinas)

Organisers: Sy-David Friedman (Kurt Goedel Research Center), John Wigglesworth (London School of Economics), Claudio Ternullo (Kurt Goedel Research Center), Neil Barton (Birkbeck College), Carolin Antos-Kuby (Kurt Goedel Research Center)

Conference Website: sotfom [dot] wordpress [dot] com

Further Inquiries: please contact
Carolin Antos-Kuby (carolin [dot] antos-kuby [at] univie [dot] ac [dot] at)
Neil Barton (bartonna [at] gmail [dot] com)
Claudio Ternullo (ternulc7 [at] univie [dot] ac [dot] at)
John Wigglesworth (jmwigglesworth [at] gmail [dot] com)

The conference is generously supported by the Mind Association, British Logic Colloquium, and Birkbeck College.

Free Schlick!

Submitted by Richard-Zach on Tue, 10/14/2014 - 12:03pm

Did you know? The Moritz Schlick Gesamtausgabe is available for free at the Moritz-Schlick-Forschungsstelle! Just click on the cover image to download the PDF (instead of the "order online" link).  Alas, it's only in German.

Cambridge Graduate Conference on the Philosophy of Mathematics and Logic

Submitted by Richard-Zach on Mon, 10/13/2014 - 8:16am

If you're in that part of the world (or will be in January), you might be interested to know that registration for the 8th Annual Cambridge Graduate Conference on the Philosophy of Mathematics and Logic (17-18 January 2015) is now open:

The conference will be held in St. John's College, Cambridge. There will be two keynote speakers and six talks from graduate students on a variety of topics in the Philosophy of Mathematics and Logic, broadly construed. The graduate papers will have respondents, and the talks will be followed by open discussion. The keynote speakers this year are Prof Alan Weir (Glasgow) and Dr Mary Leng (York)To register for the conference please click here. Registration will close on Monday the 1st of December 2014.

For more information please see the conference website:
http://www.phil.cam.ac.uk/events/camb-grad-conf-2015

Visiting Research Chair in Logic or Philosophy of Science at the University of Calgary

Submitted by Richard-Zach on Wed, 03/19/2014 - 6:27pm

US$25,000 for 4 months (September 2015 or January 2016)

Contact: Brad Hector, Fulbright Canada Program Officer (Scholars)

The University of Calgary is pleased to offer the opportunity for a Fulbright Visiting Research Chair in Logic or the Philosophy of Science. The visiting researcher will be a part of the Department of Philosophy and collaborate with a dynamic research faculty and graduate students. The Department of Philosophy is internationally recognized in logic and the philosophy of science and home to 22 professors, including a Tier 1 Canada Research Chair in the philosophy of biology. The scholar will offer a combined seminar for senior undergraduate students and graduate students in his or her area of expertise, and will participate in departmental and interdisciplinary research groups while pursuing his or her own research projects. 

Specialization: History and philosophy of science, mathematical and philosophical logic.phil.ucalgary.ca

Applicants are encouraged to identify their primary and alternate choices on the application. Formal letters of invitation should not be sought; however, applicants are encouraged to contact the institution to discuss research interests. 

http://www.cies.org/application-login
http://www.fulbright.ca/programs/american-scholars/primary-awards/science/

Leslie Lamport wins Turing Award

Submitted by Richard-Zach on Tue, 03/18/2014 - 9:16am

The Association for Computing Machinery has awarded the 2013 Turing Award (the Computer Science equivalent of the Nobel Prize Fields Medal Schock Prize) to Leslie Lamport at Microsoft Research for his work on formal specification and verification techniques, specifically the Temporal Logic of Actions and his work on fault tolerance in distributed systems. Not as close to logic as some other Turing Laureates (is that what they're called?) but still a nice nod to the continued importance of formal methods derived in part from logic in CS. (Oh yeah, he also invented LaTeX.)

Site Feed

Subscribe to Syndicate