Questions on proof assistants

[Joe Shipman]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200512/cdb99996/attachment-0001.html>