HN Explorer

Show HN: Sostactic – polynomial inequalities using sums-of-squares in Lean (github.com)

14 points by mmaaz ↗ HN
Current support for nonlinear inequalities in Lean is quite limited. This package attempts to solve this. It contains a collection of Lean4 tactics for proving polynomial inequalities via sum-of-squares (SOS) decompositions, powered by a Python backend. You can use it via Python or Lean.

These tactics are significantly more powerful than `nlinarith` and `positivity` -- i.e., they can prove inequalities they cannot. In theory, they can be used to prove any of the following types of statements

- prove that a polynomial is nonnegative globally - prove that a polynomial is nonnegative over a semialgebraic set (i.e., defined by a set of polynomial inequalities) - prove that a semialgebraic set is empty, i.e., that a system of polynomial inequalities is infeasible

The underlying theory is based on the following observation: if a polynomial can be written as a sum of squares of other polynomials, then it is nonnegative everywhere. Theorems proving the existence of such decompositions were one of the landmark achievements of real algebraic geometry in the 20th century, and its connection to semidefinite programming in the 21st century made it a practical computational tool, and is what this software does in the background.

2 comments

[ 6.2 ms ] story [ 18.6 ms ] thread
[dead] nigardev
[flagged]
mmaaz
great q! there's a variety of levers here. for one, it uses newton polytope pruning to prune the monomial basis -- this often helps a lot in practice, especially for sparse polynomials. also, both the lean and python interfaces allow to pass degree bounds in the case of a ratio of SOS, as well as a template for the denominator (e.g., ax^2 + ay^2), which also cuts down on the monomials, as well as possibly introducing affine constraints tying coefficients together. of course, in the positivstellensatz case, you can also specify the degree bound.

I wrote about all these tricks here https://mmaaz.ca/writings/sostactic.html.

and yeah, there is a clli interface for the python backend, the lean interface calls the cli.