Questions on proof assistants

[mario chiari]

Hi,

I hope you are all well. 

Is there a mailing list of the proofs assistants community to which I may ask to
subscribe? 

I mean, a list open to people which are interested to the different developments
and the general issues, not just to a single project. 

Thanks
Stay safe
mario 



On Tue, 2020-05-12 at 09:11 -0400, Joe Shipman wrote:
> 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