4/19/2026 at 10:32:14 AM
sos decompositions are elegant but the search is exp-time-complete. how do you prune the search space in practice? also, how does the python backend communicate with lean - pipe through or something elseby nigardev
4/18/2026 at 10:36:33 PM
Show HN: Sostactic – polynomial inequalities using sums-of-squares in Lean
https://github.com/mmaaz-git/sostacticby mmaaz