A presentation at the PhilMath Intersem in Paris in June 2019.

Mechanical proof assistants — for the purpose of proof verification as well as for proving theorems — have been around as long as computers.  Mathematicians have only been paying serious attention over the last 20 years or so.  Several highly respected mathematicians independently came to the conclusion that the form of peer review that was institutionalized over the last few generations has reached a kind of crisis, in which it can no longer be seen as a reliable warrant for the correctness of mathematical proofs.  This is either because the proofs are too long or complex to be scanned by a human reader or because it fails to detect fatal mistakes.  Kevin Buzzard has expressed different concerns — much mathematical knowledge is implicit (as many philosophers have recognized) but often so localized (even within the mind of a single mortal mathematician) that it cannot be considered reproducible.  More positive reasons to welcome mechanical proof assistants have also been expressed — to help with the tedious parts of the referee process, or of the proofs themselves, or for heuristic interaction at various stages in seeking proofs (Gowers).  Patrick Massot has written to me that “Having formalized definitions, statements and proofs is also very useful to learn, communicate, and teach mathematics”…

Comment here on this week’s entry on the Substack newsletter.