A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations

What is it about?

Interactive Theorem Provers (ITPs) are complex tools allowing one to encode mathematical theories and algorithms in a formal language, formulate theorems on these algorithms, develop proofs for these theorems, and mechanically check the formalized proofs with a high level of guarantee. In this work, we specifically rely on the Coq tool, of the most used tools in the ITP community. It has a very expressive logic, several tactic languages focusing on proof development, builtin support for computation, as well as support for proof reflection (roughly, the ability to perform proofs by computation). In this paper, we present the validsdp library - https://github.com/validsdp/validsdp/ - which gathers Coq tactics that can automatically and formally prove inequalities on multivariate polynomials involving real-valued variables and rational constants. These tactics internally rely on proof reflection, floating-point arithmetic, and SDP solvers (using semidefinite programming), following a certifying-based methodology that ensures we can fully trust the automatic proofs, despite the fact the external solvers are unverified and produce approximate solutions.

Featured Image