If a polynomial is everywhere non negative, it is a sum of square of rational fraction (which is the positive solution of Hilbert's 17th problem). This is an example of a certificate for positivity (more precisely non-negativity), i.e. an algebraic identify certifiying that the polynomial is non-negative.

But how to construct this sum of squares from a proof of the non negativity?

Artin's initial proof of Hilbert's 17th problem in 1927 was very indirect, and did not produce explicitely the sum of squares. Effective methods have been designed since then (starting from Kreisel and his students) but the degree estimate of the corresponding constructions were primitive recursive functions.

In this talk, we recall the initial proof of Artin and present a new constructive proof for Hilbert's 17th problem, and show that following this construction, the degree of the polynomials in the identity is bounded by an elementary recursive function in the number of variables, and the degree of the polynomial (more precisely a tower of five exponentials). We end with a discussion on what could be hoped for.

Based on joint work with Henri Lombardi and Daniel Perrucci.

Video Recording