Automatically proving polynomial positivity using numerical solvers, floating-point computations, and Rocq formal proofs

par Erik Martin-Dorel (IRIT)

jeudi 12 nov. 2026, 16:00 → 17:00 Europe/Paris

Pellos (1R2 - 207) (IMT)

Interactive theorem proving (using a theorem prover such as Rocq, Lean, or Isabelle) has been successfully used in safety-critical systems (including compilers or cryptosystems) and in many mathematical domains, where asserting the correctness of a result is paramount or error-prone. This methodology allows one to encode mathematical background, formally reason about algorithms and their correctness proof, and automatically check the formalized proofs.
In this talk, I will give an overview of the domain, then present a Rocq library (ValidSDP), co-developed at ONERA and IRIT: this contributed library offers automatic Rocq tactics that make it possible to automatically and formally prove multivariate polynomial inequalities within Rocq, using SDP solvers, but going beyond their inherent rounding errors.
The talk will be given in French, with slides in English.