The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

I would advise you to have a look on the Coq wiki:
http://coq.inria.fr/cocorico/
but aside
http://coq.inria.fr/cocorico/SquareRootTwo
I didn't see what might interest you, but maybe you
could have a second look on the wiki.

What kind of proof interest you?

-> very simple proofs on peano arithmetic
 (associativity, commutativity, ...)
-> more consistent proofs
 (prime numbers are not finite ...)
-> short proofs but on some "more complex" objects
 (Sylow theorems on groups, ...)
-> pure logical proofs not involving arithmetic at all
 (drinker's paradox, ...)
-> others?

I do not pretend to be able to do proofs for all of these,
but if you have some more precise idea of what you want,
maybe I can do some for you (but I think I have none which are
already done and waiting to be sent here).

Le Thu, 12 May 2011 12:29:49 +0200,
MailingList Bruno Woltzenlogel Paleo
<bruno.wp.mailinglist AT googlemail.com>
 a écrit :

> Hi,
> 
> I am interested in intuitionistic mathematical proofs formalized in
> Coq and satisfying (some of) the following (subjective) requirements:
> 1) it should be not too complex and not too long.
> 2) it should use some "mathematically interesting" lemma or auxiliary
> theorem. 3) obtaining an alternative proof of the same theorem not
> using the mentioned auxiliary lemma should, if possible, be
> "desirable".
> 
> If you could point me some examples of Coq proofs satisfying these
> requirements, that would be great!
> 
> Thanks in advance,
> Best regards,
> 
> Bruno
> 
> --
> Bruno Woltzenlogel Paleo
> http://www.logic.at/people/bruno/