数学形式化新突破：Sostactic工具利用SOS算法增强Lean4证明能力

针对Lean4在非线性不等式证明方面的局限，新开源工具Sostactic提供了强大的解决方案。该工具结合Python后端，利用“平方和”（SOS）分解技术，能够处理比现有`nlinarith`策略更复杂的多项式不等式。它不仅能证明多项式的非负性，还能验证半代数集合的性质及系统的不可行性。其核心技术基于实代数几何与半定规划的深度结合，将20世纪的理论成果转化为21世纪的实用计算工具，显著提升了数学自动化的边界。