Questions on proof assistants

Thu May 14 06:35:13 EDT 2020

Dear Joe, all,

some comments on your questions 1-3:

*1) which of these can make use of work done in which other ones?*

I agree here with the comment by Frederic and also the point made by Kevin.

*2) which of these would be the easiest for mathematicians with some
programming experience to learn to use to create machine-verifiable proofs?*

I prefer Isabelle/HOL and my students at FU Berlin in lecture usually have
little problems getting familiar with it (especially when working in
groups). Pros of Isabelle/HOL include the excellent proof automation
support via sledgehammer (which provides a link to various powerful
first-order and higher-order ATPs) and which in particular also supports
automated (counter-)model finding. Having strong proof automation can be of
great help, since the resources one has to spent into interactive proof are
reduced.

Generally, I do not believe anymore that senior mathematicians can easily
be converted to fruitfully work with proof assistants. It is rather the
younger generation of interdisciplinary trained young researchers (maths,
CS, philosophy) that we should focus on. And if these younger researchers
then cooperate with senior researchers in formalisation works, some real
progress can be expected.

Here are some examples of such works by young students in interaction with
senior researchers:

—  A very recent formal analysis (in Isabelle/HOL) of Gödel’s
incompleteness theorems from the perspective of paraconsistent logic, with
a high degree of proof automation, conducted by my student David Fuenmayor
(he did this together with Walter Carnielli):
https://www.cle.unicamp.br/eprints/index.php/CLE_e-Prints/article/view/1362

—  Bachelor thesis project by Lucca Tiemens (jointly supervised with Dana
Scott and Miro Benda), recent paper at RAMICS, Exploration of a Categorical
Axiomatization of Modeloids: https://arxiv.org/abs/1910.12863

I have more formalisation examples by students to share (in particular in
Metaphysics), but the above pointers should already give you an impression
on how this interaction between young and experienced researchers can work
out well.

*3) which of these have a good translator that turns a machine-readable
proof into something a human reader might gain insight from?*

In my own work I often gain insights not so much from final proofs, but
rather from countermodels by model finders to false conjectures (during an
exploration process). These countermodels may in fact help to detect issues
and misconceptions early on. For example, in joint work with Dana Scott,
see here https://doi.org/10.1007/s10817-018-09507-7, we gained insights
from such countermodels (generated by Nitpick and Nunchaku in Isabelle/HOL)
in the exploration of axiom sets for category theory, and we also revealed
(some minor) issues in a textbook using this technology.

Best wishes,

    Christoph

*--*
*Christoph Benzmüller, *Prof. Dr. habil. (http://christoph-benzmueller.de)
Freie Universität Berlin, Dep. of Mathematics and Computer Science

On Thu, 14 May 2020 at 06:53, Timothy Y. Chow <tchow at math.princeton.edu>
wrote:

> I have had some interesting discussions with Kevin Buzzard about Lean.
> Buzzard is convinced that Lean is the way to go for mathematicians.  One
> of the big selling points is that (he claims) of all the proof assistants,
> it has implemented the largest fraction of the standard undergraduate
> mathematics curriculum.  I do think that this is an important selling
> point, and it is somewhat surprising that the other proof assistants
> haven't accomplished this already.  But there are of course sociological
> reasons behind this.
>
> A couple of years ago, Tom Hales wrote a very interesting review of Lean.
>
>
> https://jiggerwit.wordpress.com/2018/09/18/a-review-of-the-lean-theorem-prover/
>
> I would say that the main reason I haven't dived into Lean is that it
> seems not to have stabilized yet.  Lean version 3 is not compatible with
> Lean version 2, and Lean version 4 (which isn't ready yet) will not be
> compatible with Lean version 3.  Lean version 4 may address some of
> Hales's criticisms but at the cost of breaking many of the existing
> libraries (which, as I said, are one of the best features of Lean).
>
> There is also the problem that there still isn't very good documentation
> that is user-friendly for the average mathematician who is not a skilled
> programmer.  But this criticism is not unique to Lean.  There's a bit of a
> vicious circle here: Mathematicians don't show much interest in proof
> assistants in part because the documentation and user interface are not
> designed with mathematicians in mind, and the documentation is the way it
> is because mathematicians haven't shown much interest.
>
> Tim
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200514/e51b113a/attachment-0001.html>