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