coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq proof of Puiseux's theorem completed
Date: Thu, 18 Sep 2014 10:56:58 +0200

Thanks John!

On Sun, Sep 14, 2014 at 02:04:21PM +0100, John Wiegley wrote:
> >>>>> 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

--
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/

[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