The Coq mailing list

[MailingList Bruno Woltzenlogel Paleo <bruno.wp.mailinglist AT googlemail.com>]

Thanks for your answer.
Sorry that my previous email was a bit vague about what kind of mathematical proofs would interest me.
I hope the longer info below will clarify this.

Here in my group in Vienna we are developing a cut-elimination method called CERes (Cut-Elimination by Resolution) and we are insterested in employing this method to eliminate cuts/detours from mathematical proofs, in the hope of finding simpler mathematical proofs. One of our success stories is the elimination of cuts from Fuerstenberg's proof of the infinity of primes, which contains cuts/lemmas from Topology. After elimination of these cuts with the CERes system, we obtained a "simpler" formal proof that corresponds to Euclid's proof of the infinity of primes and has not topological lemmas.

The current CERes method works for classical logic, and we would like to try to extend it to intuitionistic logic. Moreover, proof formalization is one of the bottlenecks in our process, and it would be great if we could use proofs already formalized in proof assistants.
That is why I asked for formalizations of intuitionistic mathematical proofs in Coq.

The proof of irrationality of square root of two has a lemma, but it is just a restatement of the theorem using integers instead of rationals. So, it wouldn't be so interesting to eliminate this lemma.

So, I am looking for some proof with detours/cuts/lemmas that are "interesting" to eliminate (as in the case of Fuerstenberg's proof), that are not too long (hopefully much smaller than Fuerstenberg's proof) and that are intuitionistic, and of course formalized in Coq. Any field of mathematics is fine.

If you know some proof satisfying these requirements, please let me know. We would try to use this proof as a benchmark during the development of the CERes method for intuitionistic logic. And maybe one day (in the very distant future) we could return the favor, if our methods end up maturing into a proof transformation system that could interact with Coq...

Best regards,

Bruno

--
Bruno Woltzenlogel Paleo

On May 12, 2011 1:55 PM, "AUGER Cedric" <Cedric.Auger AT lri.fr> wrote:
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...