coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club]Formalizing 100 theorems

From: Laurent Th�ry <Laurent.Thery AT sophia.inria.fr>
To: herman AT cs.ru.nl, Yves.Bertot AT sophia.inria.fr, Milad.Niqui AT cs.ru.nl, Frédérique.Guilhot AT sophia.inria.fr, r.oconnor AT cs.ru.nl, lcf AT math.ist.utl.pt, Hugo.Herbelin AT inria.fr, gonthier AT microsoft.com, synek AT cs.kun.nl, martijno AT cs.ru.nl, Julien.Narboux AT inria.fr, Loic.Pottier AT sophia.inria.fr, Coq Club <coq-club AT pauillac.inria.fr>, Laurent Th�ry <Laurent.Thery AT sophia.inria.fr>, freek AT cs.ru.nl
Subject: [Coq-Club]Formalizing 100 theorems
Date: Fri, 30 Mar 2007 13:14:56 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear Coq Users,

Freek Wiedijk is maintaining a list of 100 mathematical theorems to be
formalised

http://www.cs.ru.nl/~freek/100/

Of course, such a list is subjective but I think it could be very
useful for comparing provers and evaluating what each prover
can actually achieve on a fixed set of examples.
That's why I propose myself to collect all the formalisations done in Coq.
and turn them into a single contribution inside Coq.

If you have formalised one of these theorems (or you plan to),
I will be very happy if you can send me a version of your formalisation
so I can include it to the contribution.
Packaging your contribution to make its integration to the contrib
as smooth as possible, would be greatly appreciated.

Regards,

--
Laurent Th�ry

[Coq-Club]Formalizing 100 theorems, Laurent Th�ry