Questions on proof assistants

[Frédéric Blanqui]

Hello.

Le 12/05/2020 à 15:11, Joe Shipman a écrit :
> I see on Freek Wiedijk’s page
>
> http://www.cs.ru.nl/F.Wiedijk/100/index.html
>
> that proof assistants are doing reasonably well at formalizing the 
> “top 100” theorems:
>
> HOL Light 86
> Isabelle 83
> Metamath 74
> Coq 70
> Mizar 69
>
> My questions are:
> 1) which of these can make use of work done in which other ones?

Interoperability between proof assistants is currently very limited. In 
theory, you should be able to reuse HOL Light proofs in Isabelle using 
the OpenTheory format but some information is lost in between. There is 
also https://www.lri.fr/~keller/Recherche/hollightcoq.html to reuse HOL 
Light proofs in Coq, and there is an ongoing work on translating Mizar 
proofs in Isabelle using automated theorem provers.

http://deducteam.gforge.inria.fr/ develops a framework, the 
lambda-Pi-calculus modulo rewriting, for translating proofs from one 
system to the other. See http://www.lsv.fr/~dowek/Publi/expressing.pdf 
and http://www.lsv.fr/~fthire/ . Various tools have been developed for 
translating proofs from various systems (Coq, Matita, Isabelle, Agda, 
OpenTheory, PVS) to this framework and back. See 
http://logipedia.inria.fr/about/about.php to see an example of library 
of arithmetical lemmas translated from Matita to OpenTheory, Coq, Lean 
and PVS. A type/proof checker for the lambda-Pi-calculus modulo 
rewriting is implemented in https://deducteam.github.io/. A new 
interactive version is under development on 
https://github.com/Deducteam/lambdapi/ .


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

Having a programming experience may be useful for some systems but why 
would it be necessary in general?


> 3) which of these have a good translator that turns a machine-readable 
> proof into something a human reader might gain insight from?
>
Almost none, except those whose proof scripts are close to natural 
language already, namely Mizar. There has been some works in automatic 
translation of lambda-calculus proofs into natural language in the 80's 
or 90's but they are not been used a lot and may not scale up.

Best regards,

Frédéric Blanqui.