Questions on proof assistants

[Joseph Vidal-Rosset]

Hello,

I believe that it would be good to add Athena
http://www.proofcentral.org/athena/  in this list,
and also  this book:
https://mitpress.mit.edu/books/fundamental-proof-methods-computer-science
to learn this language for proof and computation invented by
Konstantine Arkoudas.

Best wishes,

Jo.



Le mer. 13 mai 2020 à 01:42, Joe Shipman <joeshipman at aol.com> 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?
> 2) which of these would be the easiest for mathematicians with some programming experience to learn to use to create machine-verifiable proofs?
> 3) which of these have a good translator that turns a machine-readable proof into something a human reader might gain insight from?
>
> — JS
>
> Sent from my iPhone