Show HN: Sostactic – polynomial inequalities using sums-of-squares in Lean

Category: devtools

Tags: theorem-proving, polynomial-optimization, formal-verification

Score: 7.0/10 (Innovation: 8, Technical: 8, Documentation: 8, Utility: 4)

Sostactic is a Lean4 tactic suite for proving polynomial inequalities using sum-of-squares decompositions, powered by a Python backend that solves semidefinite programs. It's interesting because it bridges formal theorem proving (Lean) with numerical optimization (cvxpy) to automatically generate exact, verifiable certificates for problems beyond the reach of standard tactics like nlinarith.

Target audience: formal methods researchers, mathematicians, Lean users

Repository: https://github.com/mmaaz-git/sostactic · Python · 20 stars

View on Hacker News