Questions on proof assistants

[Prof. Julian Rohrhuber]

It might be really good to do something like http://rosettacode.org/ for proof assistants: different (possibly simple) proofs or tasks done in different systems.

[please excuse the repeated post, Joe and Joseph, I had technical problems]


> On 14. May 2020, at 20:47, Joseph Vidal-Rosset <joseph.vidal.rosset at gmail.com> wrote:
> 
> 
> 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