In this work we present two algebraic certificates for Budan's theorem. Budan's theorem claims the following. Let R be an ordered field, f in R[X] of degree n and a,b in R with a

Dans ce travail, nous présentons deux certificats algébriques pour le théorème de Budan. Le théorème de Budan s'énonce comme suit : Soit R un corps ordonné, f in R[X] de degré n et a,b in R avec a<b. Alors, le nombre de variations de signe dans la suite (f(b),f'(b),...,f^n(b)) n'est pas supérieur au nombre de variations de signe dans la séquence (f(a),f'(a),...,f^n(a)). Cela nous permet de compter des racines réelles d'une manière similaire au comptage des racines réelles par le théorème de Sturm. (Compter des racines réelles à la Budan est aujourd'hui connu comme Budan-Fourier count. En effet, il compte des racines dites virtuelles qui comprennent les racines réelles.) Un certificat algébrique pour le théoème de Budan est un certain type de preuve qui mène de la négation de l'hypothèse à l'identité algébrique contradictionelle 0>0. L'algorithme pour notre premier certificat est basé sur la preuve historique par Budan, qui utilise uniquement des arguments combinatoires. Il a une complexité exponentielle dans le degré de f. L'algorithme pour le deuxième certificat est basé sur des suites de Taylor mixtes et exhibe une plus petite complexité : Le calcul principal est la résolution d'un système linéaire, ce qui est polynomiale dans le degré de f / In this work we present two algebraic certificates for Budan's theorem. Budan's theorem claims the following. Let R be an ordered field, f in R[X] of degree n and a,b in R with a<b. Then the number of sign changes in the sequence (f(b),f'(b),...,f^n(b)) is not greater than the number of sign changes in the sequence (f(a),f'(a),...,f^n(a)). This enables us to count real roots in a similar way to the real root counting by Sturm's theorem. (Budan's count of real roots is today known as ``Budan-Fourier count'' which, indeed, counts so called virtual roots which comprehend the real roots.) An algebraic certificate for Budan's theorem is a certain kind of proof which leads from the negation of the assumption to the contradictory algebraic identity 0>0. The algorithm for our first certificate is based on the historical proof by Budan which uses only combinatorial arguments. It has a complexity exponential in the degree of f. The algorithm for the second certificate is based on mixed Taylor series and shows a smaller complexity: The main calculation is solving a linear system; this is polynomial in the degree of f.