The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Wed, Nov 26, 2014 at 09:35:11AM +0100, Carst Tankink wrote:
> In any case, thanks for posting this, Gabriel! It's always good to have
> something on the web to point to when making the point that theorem provers
> need external support (tools/documentation/communities) as well as the tool
> itself.

I fully agree.  Unfortunately the wish-list is so long that it makes me
fear it will take a century to solve all these issues.

But I really want to share the solution to one of them, in particular
how to prove the infinity of primes on top of a "well furnished"
library[1] in a number of lines that compares well with his latex proof:

  https://sympa.inria.fr/sympa/arc/ssreflect/2014-04/msg00000.html

Best,
-- 
Enrico Tassi
[1] : that Neil could not install, and that is very sad, but still...