Mathematical Conversations

Constructive vs Pure Existence proofs have been a topic of intense debate in foundations of mathematics. Constructive proofs are nice as they demonstrate the existence of a mathematical object by describing an algorithm for building it. In computer science, we, in fact, have to worry about the algorithm itself being efficient. On the other hand, constructive proofs can be quite restrictive in that, they may not be as illuminating or natural to come up with as a non-constructive proof.In this talk, I will explain a method where we can have our cake and eat it too. I'll describe a restricted system of proofs that allows us to work essentially unfettered by the restriction of constructiveness and come up with proofs ``as is'' and still guarantee an automatic translation of our proofs into efficient algorithms. The technical workhorse of this method is the observation that the positivstellensatz theorems (due to Artin, Putinar, Stengle and others) are efficiently constructive: whenever a non-negative multivariate polynomial over the reals has a proof of non-negativity via an equivalent representation as a sum of squares of low-degree polynomials, there's also an efficient algorithm to find such a representation.Far from just being an intellectual curiosity, this sum-of-squares method of coming up with proofs is remarkably powerful. It not only captures and illuminates classical results in algorithm design, but also yields the state-of-the-art algorithms for many basic algorithmic questions in computer science.