The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

My five axioms:

1/ function which returns the rank of the 1st non zero value of a power
   series, or infinity if null series
2/ property of the result of that function
3/ function which returns the best k for which a power series is in x^k
   (equal to the gcd of the rank of all non zero values of the series)
4/ property of the result of that function
5/ ∀ P : nat → Prop, { ∃ n, P n } + { ∀ n, ¬P n }.

We could say there are only 3 axioms if we count 1 and 2 together and
3 and 4 together.

I also had to add that the equality in the base field K is decidable.

On Mon, Sep 15, 2014 at 09:56:39AM -0400, 
croux AT andrew.cmu.edu
 wrote:
> Exciting! Do you mind if I ask which axioms were used?
> 
> Cody
> 
> > 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.
> >

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