id: 1964
uid: 86ri5
insdate: 2026-04-19 02:05:14
title: Show HN: Sostactic – polynomial inequalities using sums-of-squares in Lean
additional: 🎉 "Leaning on Sums-of-Squares for Polynomial Inequalities"

Sostactic leverages sums-of-squares decompositions to prove polynomial inequalities in Lean, offering a more powerful alternative to existing tactics like nlinarith and positivity. This package enables users to prove that polynomials are nonnegative globally or over semialgebraic sets, and even show that systems of polynomial inequalities are infeasible, making it a valuable tool for formal verification and mathematical exploration.
category: Hacker News
md5:
guid: https://news.ycombinator.com/item?id=47820134
source_url: https://github.com/mmaaz-git/sostactic
updated:
image:
author_name: mmaaz
author_link: