Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland


Chronological Thread 
  • From: Enrico Tassi <enrico.tassi AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland
  • Date: Wed, 26 Nov 2014 11:40:03 +0100

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...



Archive powered by MHonArc 2.6.18.

Top of Page