Questions on proof assistants

[Ingo Blechschmidt]

Dear Joe,

On Tue 12 May 2020 09:11:07 AM GMT, Joe Shipman wrote:
> that proof assistants are doing reasonably well at formalizing the
> “top 100” theorems:
> 
> HOL Light 86 
> Isabelle 83
> Metamath 74
> Coq 70 
> Mizar 69

notable proof assistants which are missing from this list include at
least Agda, Minlog and Nuprl.

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

Unfortunately, interoperability between the various proof assistants is
quite limited. To some extent this is for fundamental reasons, as they
implement non-comparable foundations; to some extent this is because no
translator has been written.

This state of affairs is unsatisfactory, since developing a standard
library is a massive undertaking and hence there is lots of duplicated
work. On the other hand, each of the proof assistants has compelling
unique features, and the foundations are only pushed if thoroughly
exercised.

To answer your question, Coq can import Lean and HOL Light; Isabelle/HOL
can import HOL4; and a couple more such pairs are listed in a survey by
Kohlhase and Rabe.

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

I guess that currently Lean is easiest to start with, because of its fun
natural number game which runs directly in the browser [2]. You can also
try Agda [3] and Coq [4] online. Isabelle also has something like this,
but I can't find a link right now.

Unfortunately all proof assistants are somewhat nontrivial to install,
especially on Windows. Good tutorials exist for all of them. I
particularly like the free online book by Philip Wadler and Wen Kokke
for Agda [5].

That said, ease of starting is certainly an important factor, and indeed
a factor where all proof assistants could still improve, but it probably
should not be the only factor for deciding on a proof assistant.

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

I have gained insights directly from Agda code, without any translation. 

In general, the code of proof assistants should definitely be readable
to humans (if they are familiar with the language). In my opinion, this is
especially so for those assistants in which we typically write *proof
terms* (as in Agda) instead of *proof scripts* (as in Coq, Isabelle and
Lean), but the opposite opinion is also widespread.

For instance, here is an Agda proof of the fact "n = n + 0" about natural numbers:

    plus-zero : (n : ℕ) → n ≡ n + 0
    plus-zero zero     = refl
    plus-zero (succ k) = cong succ (plus-zero k)
    -- we construct a witness of equality by recursion and appeal to
    -- "cong succ", a lemma stating that the successor operation preserves
    -- equality

And here is the same proof in Coq:

    Theorem plus_zero : (forall n, n = n + 0).
    Proof.
      intros n. induction n as [| n' IHn'].
      - reflexivity.
      - simpl. rewrite <- IHn'. reflexivity. Qed.
    (* instead of a recursive call, we use the induction tactic *)

Proof scripts are closer to what we are writing on a blackboard, but
without using the interactive assistant, you don't immediately see which
assumptions are in scope and what the current goal is.

There is some work on translating from and to English [6].

Cheers,
Ingo

[1] https://arxiv.org/abs/2005.03089
[2] https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/
[3] https://agdapad.quasicoherent.io/
[4] https://x80.org/rhino-coq
[5] https://plfa.github.io/
[6] https://sketis.net/2019/isabelle-naproche-for-automatic-proof-checking-of-ordinary-mathematical-texts