coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Laurent Théry <Laurent.Thery AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq proof of Puiseux's theorem completed
Date: Sun, 14 Sep 2014 22:53:39 +0200

On 09/14/2014 02:14 PM, Daniel de Rauglaudre wrote:
> 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.
>

Congrat!!

There are only 10 theorems left on Freek's list:

http://www.cs.ru.nl/~freek/100/

--
Laurent

[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