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...
- [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Gabriel Scherer, 11/25/2014
- Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Frédéric Blanqui, 11/25/2014
- Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Carst Tankink, 11/26/2014
- Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Enrico Tassi, 11/26/2014
- Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Ilmārs Cīrulis, 11/30/2014
- Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Cedric Auger, 11/30/2014
- Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Ilmārs Cīrulis, 11/30/2014
- Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Enrico Tassi, 11/26/2014
- Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Cyril Cohen, 11/26/2014
- Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Pierre Courtieu, 11/26/2014
- Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Carst Tankink, 11/26/2014
- Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland, Frédéric Blanqui, 11/25/2014
Archive powered by MHonArc 2.6.18.