University of Calgary
UofC Navigation

All LogBlog Posts

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

Steve Awodey gives inaugural Calgary Mathematics & Philosophy Lecture

Submitted by Richard Zach on Wed, 10/01/2014 - 3:17pm

I'm very excited that Steve Awodey is on his way here to deliver the first Calgary Mathematics & Philosophy Lecture tomorrow! He's speaking on "Univalence as a New Principle of Logic." If you're in Calgary, you should come.  It'll be exciting. Thursday, 3:30 pm, in Engineering Building A aka ENA 101 on the UofC campus. Here's the abstract:

It is often convenient or useful in mathematics to treat isomorphic structures as the same.  The Univalence Axiom for the foundations of mathematics elevates this idea to a foundational principle in the setting of Homotopy Type Theory.  It states, roughly, that isomorphic structures can be identified.  In his talk, Prof. Awodey will explain this principle and how it can be taken as an axiom, and explore the motivations and consequences, both mathematical and philosophical, of making such an assumption.

Steve will give a more technical talk in the Math Department on Friday at 2pm.

Also check out the sweet poster:

Milton Friedman and Gödel

Submitted by Richard Zach on Tue, 09/23/2014 - 10:51am

I've been having a conversation with Alex Douglas and Eric Schliesser on their posts (Alex's, Eric's) about Milton Friedman's footnote about observer-dependence and Gödel's incompleteness theorem.

John Venn Day

Submitted by Richard Zach on Mon, 08/04/2014 - 2:21am

John Venn would have been 180 today (August 4). In celebration, Google put up an interactive Venn Diagram doodle, which is pretty amazing.

Also, TIL that it's not a Venn diagram if it doesn't contain all possible intersections, a restriction that doesn't apply to Euler diagrams.  So representing an empty intersection by two non-intersecting regions is, technically, not a Venn diagram; and Venn diagrams for more than three sets get harder and harder to draw. Check out the informative Wikipedia entry.

I have a previous entry on humorous Venn (and Euler) diagrams around the Internets.

Gödel's Vienna: Finding Café Reichsrat

Submitted by Richard Zach on Thu, 07/24/2014 - 3:51am

The Café Reichsrat in Vienna is notable as the place where Gödel, on August 26, 1930, first announced the incompleteness theorem to Carnap, Feigl, and Weismann. The members of the Vienna Circle had met there to prepare for the trip to the "Zweite Tagung für Erkenntnislehre der Exakten Wissenschaften," a satellite meeting to the congress of the German Society of Mathematicians organized by the Vienna Circle. This was where the famous symposium on the foundations of mathematics took place, with Carnap representing logicism, Heyting intuitionism, and von Neumann speaking for Hilbert's school of formalism -- the contributions are reprinted in Benacerraf's anthology Philosophy of Mathematics. From Carnap's diary: "6-1/2 9 [6pm to 8:30pm] Cafe Reichsrat ... preparations for the trip to Königsberg. Gödel's discovery: incompleteness of the system of Principia Mathematica ... difficulties of the consistency proof."  In February 1930, Gödel and Tarski discussed logic here during the latter's first visit to Vienna.

The Reichsrat no longer exists, and the only picture that's around shows just the top of one of its doors (from Jimmy Schimanovich's photo gallery).

The window atop the door, columns, and stucco match the entrance to the Konditorei Sluka at Rathausplatz 8, and presumably on the basis of this it's long been believed that the Reichsrat used to be located where the Sluka is now. But the Sluka has been around since 1891, which led Paul Raymont to speculate that it expanded into the Reichsrat's space after the latter closed down. In 2010, Karlis Podnieks noticed that on the other side of the main driveway to Rathausplatz 8 there's another door that also looks like the one in the picture, and conjectured that the Reichsrat might have been located there. But Vienna's Kaffeehäuser were cavernous establishments and also almost all located at corners. So I asked Karl Sigmund, co-editor of Kurt Gödel: The Album and creator of the Gödel Exhibition, for help, and he suggested to check the phone book!  And indeed, Adolph Lehmann's allgemeiner Wohnungs-Anzeiger : nebst Handels- u. Gewerbe-Adressbuch für d. k.k. Reichshaupt- u. Residenzstadt Wien u. Umgebung gives the address for the Reichsrat as Stadiongasse 2.

Phone book entry for Kaffeehaus Reichsrat

The Café Reichsrat was thus located at the north-west corner of Stadiongasse and Reichsratsstraße/Rathauspark, and the archive picture probably shows the mid-block back entrance facing the Rathauspark identified by Podnieks. A bank now occupies the space:

Location of the former Café Reichsrat in Vienna

If you go visit, do have a coffee and cake at the Sluka!  I also made a map for all you Gödel pilgrims.

And here is some background reading:

John W. Dawson, Jr., Karl Sigmund, 2006. Gödel’s Vienna. The Mathematical Intelligencer 28(3), 44-55

For an almost complete list of people and places from the time of the Vienna Circle, consult:

Volker Thurm, 2003. Wien und der Wiener Kreis: Orte einer unvollendeten Moderne: Ein Begleitbuch, Vienna: facultas.wuv / maudric

Bleg: Philosophy survey for mathematicians

Submitted by Richard Zach on Mon, 07/21/2014 - 4:42am

A group of researchers in philosophy, psychology and mathematics are requesting the assistance of the mathematical community by participating in a survey about mathematicians’ philosophical intuitions. The survey is here: http://goo.gl/Gu5S4E. It would really help them if many mathematicians participated. Thanks.

The Place of Logic in Computer Science Education Followup

Submitted by Richard Zach on Thu, 07/17/2014 - 4:42am

The Special Session on "The Place of Logic in Computer Science Education" took place at the Logic Colloquium on Tuesday. It was well attended and, I think, overall a successful session.  The newly-formed ACM Special Interest Group on Logic and Computation (SIGLOG) was represented by its chair Prakash Panangaden. He stressed the importance of logicians (and computer scientists/instructors relying on logic and logical methods) to push for the integration of logical methods in the CS curriculum -- the way the SIG on Programming Languages SIGPLAN has successfully managed to give prominence to programming languages and design. In the US, the existence of a standard curriculum makes it difficult for departments that would even want to put a focus on logic and formal methods to introduce dedicated courses, a point made by Phokion Kolaitis in discussion.  That curriculum includes only propositional logic and just the very basics of predicate logic as a requirement for all CS majors. In a previous panel at a SIGCSE meeting, it was argued that a remedy would be to integrate bits of logic in other courses where logical methods are needed.  This resulted in the TeachLogic Project, led by Moshe Vardi at Rice University, which aimed to provide course materials and ideas for where and how to incorporate logic into CS courses.

In Europe, departments seem to have a lot more leeway.  This makes it possible, e.g., for Austrian CS departments to even offer specialized grad programs in logic and computing, as Alex Leitsch reported.  Nicole Schweikardt presented ideas from an introductory course she teaches in Frankfurt.  One of her didactic lessons was that engaging examples are important to draw in students -- pure logic courses tend to do a less-than-optimal job at convincing students that this stuff is useful and important.  Her "provocative statement was: "When confronting computer science students with formal logic for the first time, we should dare to be less formal." This tied in with another topic of discussion: diversity.  In the US, the gender split in CS is even worse than in philosophy: 12% of 2010-11 CS degrees were awarded to women. Byron Cook also mentioned this as an issue, and pointed to Harvey Mudd College as a success story for how to get and keep members of underrepresented groups in(to) CS.  Now Harvey Mudd is an elite college and in many places that kind of institution-wide initiative is sadly not feasible (as Phokion pointed out). 

There are lessons to be learned, not just for how we teach formal methods in CS but also for logic courses in philosophy departments. One may be to make these courses -- not: less rigorous -- but simply more appealing by focussing more on examples and applications which are familiar and engaging to a broader audience that's not already familiar with formal methods. In the discussion, Brigitte Pientka pointed out, however, that it would be a mistake to think that we have sacrifice rigor in logic or CS courses to make them appealing to women and enable them to succeed in them.  She referred to the environment at Carnegie Mellon University and the research by Carol Frieze and others who have documented that a more balanced environment allows both men and women to participate, contribute, and be successful, in the CS major, without accommodating presumed gender differences or watering down the curriculum to become "more female friendly".  Since 2002 the percentage of bachelor‘s degrees granted to women in the CS major at CMU has exceeded and stayed well above the national average. It is currently at 25%.  These and other initiatives are covered in a piece on drawing women to computer science published in the NYT's TheUpshot blog just yesterday.

SIGLOG is forming an Education Committee, which will carry on the work of the TeachLogic project and hopefully can serve as a clearing house for ideas, materials, and tools.  If you're interested in being involved, Prakash would like to hear from you!  In addition, this would be a good place to announce that the conference Tools for Teaching Logic is happening again next year!

(Cross-posted at the Vienna Summer of Logic blog.)

Summer of Logic Dance Party

Submitted by Richard Zach on Sat, 07/12/2014 - 11:22am

So there will be a student party at the Summer of Logic. Help me crowdsource logic/math/CS/AI tracks, preferably danceable. Ideas?

Pet Shop Boys - He Dreamed of Machines

Turing Machines - Slave to the Algorithm

My Robot Friend - Robot High School

Super Furry Animals - Fuzzy Logic

Daniel Avery - Drone Logic

Scooter - The Logical Song [Supertramp cover]

Squarepusher - Music for Robots

The Illuminator - 4 r square pi (Association for Symbolic Logic)

Or I guess we can just play Logic all night:

Logic - Mind of Logic / The Spotlight / ...

or A-Track's "Infinity + 1" mix and the entire Stills album "Logic will Break your Heart."

Joachim Lambek (1922-2014)

Submitted by Richard Zach on Sat, 06/28/2014 - 7:54am

More sad news, via the Studia Logica list:

We sadly inform that Professor Joachim Lambek (Jim for friends) passed away on June 23, 2014, at 2:00 p.m. in Montreal.

Joachim Lambek was born in Leipzig on December 5, 1922. His parents moved to Leipzig from a small town near Krakow (Poland). In the late 1930-ties the family left Germany for England. After the outbreak of the SWW, he spend two years in an internment camp in Canada, then entered McGill University in Montreal. He earned Ms.C. in mathematics in 1946. This university has remained his affiliation throughout his academic career; in the years 1963-1993 he was a professor at the Department of Mathematics and Statistics and occupied the Peter Redpath Chair, then a professor emeritus at McGill. He has visited many universities and research centers in Europe and America.

J. Lambek's scientific interests focused on algebra, category theory, mathematical logic, mathematical linguistics and number theory. In category theory he developed categorical logic, e.g. he has shown close connections between cartesian closed categories and typed lambda calculi. In mathematical linguistics, Lambek's Syntactic Calculus, introduced in 1958 (nowadays called Lambek Calculus), is a basic logic for modern type grammars. This calculus and its different variants are extensively studied also in algebraic logic as the basic substrutural logics. In the last decades J. Lambek developed an algebraic approach to grammar, involving pregroups. He also studied some algebras of physics (quaternions) and published books on the history of mathematics.

Getting Excited about the Computational Logic Olympics

Submitted by Richard Zach on Thu, 06/19/2014 - 11:19am

So while everyone is following the World Cup, I'm getting excited about the FLoC Olympic Games to be held at the Vienna Summer of Logic this year.  Still doing my research to pick favourites, but here are some of the disciplines:

plus a few others.  There will even be live viewing and a medal ceremony!

Grigori Mints, 1939-2014

Submitted by Richard Zach on Fri, 05/30/2014 - 5:46am

(C) George BergmanVery sad news today: Grisha Mints has died.  He was born June 7, 1939 in Leningrad (now St. Petersburg). He received his education in mathematics at Leningrad State University under N. A. Shanin, and held positions there, at the Steklov Institute in Leningrad, and then, from 1980-1991, at the Estonian Academy of Science in Tallinn.  In 1991 he joined the Philosophy Department at Stanford University, where he also held courtesy appointments in computer science and mathematics (since 1992 and 1997, respectively).  In 2008 he was elected to the Estonian Academy of Sciences, and in 2010 named a fellow of the American Academy of Arts and Sciences.

Grisha was a force in logic, especially in proof theory.  His early work centered on systems for automated theorem proving, where he contributed significantly to the development of Maslov's inverse method, resolution, and the relation between the two. He made major contributions to general proof theory, non-classical logics, constructive mathematics, program verification, and proof mining. He was the leading expert on Hilbert's epsilon calculus and the substitution method approach to the proof theory of strong subsystems of arithmetic. In addition to over 200 papers, he wrote two introductory books on modal and intuitionistic logic, and some of the early papers from his days in the Soviet Union were collected in his Selected Papers in Proof Theory.

I'm grateful to have had many beautiful interactions with Grisha over the years.  The logicians at the TU Vienna had close contacts with Tallinn in the late 80's and early 90's, and I had the good fortune to meet Grisha then. While at Berkeley and Stanford, I attended a couple of his classes. He was a demanding teacher, but I learned a lot.  I often visited before I taught at Stanford, and a few times since I've left. Whenever I did, he would ask me what I was working on, and he'd acknowledge what I'd said with a smile and a sideways nod and "um-hmm."  Often he would then tell me about some obscure, usually Soviet-era, book or paper that addressed all the problems and questions I had. Then came the part where he'd tell me about his current work, and I would struggle to keep up.  I'll always fondly remember those visits. He was a wonderful, generous teacher and colleague.

UPDATE: Memorial notice from Stanford's department chair Lanier Anderson.

Simple Way to Document Code with Markdown, grep, and pandoc

Submitted by Richard Zach on Thu, 05/29/2014 - 2:26pm

Here's a simple way to pretty-print documentation included as comments in a source file (I'm mainly interested in LaTEX code), with or without the intervening code.  It's useful if you don't want to bother with a more complicated solution such as LaTeX's docstrip + ltxdoc.  It uses the ubiquitous bash tools grep and cut (available on Linux and probably (?) on Mac OS) plus John MacFarlane's pandoc , which you might have to install separately.

Include your documentation in the source file as comments, i.e., in LaTeX, on lines which start with %. Make sure they in fact start with "% ", i.e., % followed by a space. Your documentation can use any format pandoc understands, but Markdown is probably the simplest.  Your comments will be easily readable in the source file, but you can include markup, e.g., # headers, *italicized* or **boldface**, `code`, \$math\$, itemized lists, etc. Because your documentation is a regular comment that doesn't have to be stripped for the file to compile, you can use/compile your source file as you ordinarily would without running it through a pre-processor. To get the documentation, you filter out the non-commented lines, removethe comment signs, and run them through pandoc.

First, we have to filter out the non-comment lines from the source file and throw away the rest. This can be done using grep:

    grep -e "^%" -e "^$"

The first filter "^%" matches any line beginning with a %, the second "^$" matches empty lines (so you get paragraph breaks between documentation blocks in the output).

Then you want to strip the initial comment character; in fact, we can just throw away the first two characters of every remaining line, using the cut command

    cut --bytes=3-

The result is a file in Markdown format which you can now run through pandoc to create your favorite output, e.g., HTML or PDF.

    pandoc -f markdown -t html

You can put all of this together into a pipe, or make a bash script, or use it in a Makefile target. For instance, if you save the following as "makedoc"

    #!/bin/bash

    grep -e "^%" -e "^$$" $1.tex | cut --bytes=3-| pandoc -f markdown  -o $1.pdf

you can use "./makedoc <mytexfile>" to produce a PDF of the documentation included in <mytexfile>.tex in <mytexfile>.pdf. (Note the double $$ and make sure you make the file executable, e.g., via chmod u+x makedoc).

To set title, author, and date of the documentation, include them, preceded by an extra "% " in the first three lines of your file (in that order).

The procedure above will filter out the comments and turn them into the documentation, e.g., a user guide or something like that.  You can also set it up to print a documented source by beginning and ending every block of code with a commented "code fence", i.e., a line that contains "% ```" (%, space, three backticks). Then we'll run the file first through sed and tell it to remove all the "% " at the beginning of a line.

    sed "s/^% *//" $1.tex | pandoc -f markdown -o $1.pdf

Extra geek points for the person to come up with a sed command to print any commented line and all lines between code fences but remove code not between code fences!

UPDATE: The extra geek points go to Mark van Atten who sent in this solution using awk:

 awk '/^% ```/ {print substr($0,3,length($0)-2) ; printcode=1-printcode;next } printcode {print;next} /^% / {print substr($0,3,length($0)-2);next} /^[ \t]*$/ {print}'  $1.tex | pandoc -f markdown  -o $1.pdf 

Pages

Site Feed

Subscribe to Syndicate