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.
[flagged]
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.