coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] Coq proof of Puiseux's theorem completed
Date: Sun, 14 Sep 2014 14:14:28 +0200

Dear all,

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.

Regards.

--
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