Muhammad Maaz released Sostactic, a set of Lean4 tactics that proves polynomial inequalities using sum-of-squares decompositions. It handles problems that stump existing Lean tactics like nlinarith and positivity. The tool can prove global polynomial nonnegativity, nonnegativity over semialgebraic sets defined by polynomial constraints, and emptiness of semialgebraic sets. The repo includes examples like the AM-GM inequality and the Motzkin polynomial.
The clever bit is the architecture. Lean calls a Python CLI powered by cvxpy, a convex optimization library, which solves semidefinite programming problems. The catch: SDP solutions are numerical, floating-point approximations. Theorem provers need exact answers. Sostactic converts numerical solutions into exact certificates through rationalization and projection techniques that Lean can verify. Sometimes exactification fails. When it does, the solver tells you what to try next.
This approach isn't new. HOL Light, Isabelle/HOL, and Coq all have similar integrations. But Sostactic brings it to Lean4 with a Python backend that can use modern optimization libraries. The math behind it comes from Positivstellensatz theorems in real algebraic geometry, which establish when positive polynomials can be written as sums of squares. Pablo Parrilo and others turned this theory into a practical computational tool in the early 2000s.
Maaz built Sostactic with formalization help from Moeez Muhammad. The package tracks Mathlib v4.29.0-rc8 and needs Python 3.10+. It works as a Python API, a Python CLI, or directly as Lean tactics. For people working in control theory, robotics, or systems verification where polynomial inequalities model safety constraints, having these proofs inside a theorem prover gives formal guarantees that engineering tools like SOSTOOLS and YALMIP can't match, just like verifying Apollo 11 code.