coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq proof of Puiseux's theorem completed

From: "John Wiegley" <johnw AT newartisans.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq proof of Puiseux's theorem completed
Date: Sun, 14 Sep 2014 14:04:21 +0100
Organization: New Artisans LLC

>>>>> Daniel de Rauglaudre
>>>>> <daniel.de_rauglaudre AT inria.fr>
>>>>> writes:

> I am glad to announce you that I just finished a formal proof in Coq
> of Puiseux't theorem: 18 months of work, 250 definitions, 5 axioms,
> 1200 theorems. Source soon available.

Congratulations!!

John

[Coq-Club] Coq proof of Puiseux's theorem completed, Daniel de Rauglaudre, 09/14/2014
- Re: [Coq-Club] Coq proof of Puiseux's theorem completed, John Wiegley, 09/14/2014
  - Re: [Coq-Club] Coq proof of Puiseux's theorem completed, Daniel de Rauglaudre, 09/18/2014
- Re: [Coq-Club] Coq proof of Puiseux's theorem completed, Laurent Théry, 09/14/2014
- Re: [Coq-Club] Coq proof of Puiseux's theorem completed, croux, 09/15/2014
  - Re: [Coq-Club] Coq proof of Puiseux's theorem completed, Daniel de Rauglaudre, 09/15/2014
    - Re: [Coq-Club] Coq proof of Puiseux's theorem completed, Alan Schmitt, 09/18/2014
      - Re: [Coq-Club] Coq proof of Puiseux's theorem completed, Bas Spitters, 09/18/2014
      - Re: [Coq-Club] Coq proof of Puiseux's theorem completed, Daniel de Rauglaudre, 09/18/2014
      - Re: [Coq-Club] Coq proof of Puiseux's theorem completed, Daniel Schepler, 09/18/2014