最新

目前 Lean 对非线性不等式的支持非常有限。这个软件包试图解决这个问题。它包含了一系列 Lean4 策略，用于通过平方和 (SOS) 分解来证明多项式不等式，由 Python 后端提供支持。你可以通过 Python 或 Lean 来使用它。 这些策略比 `nlinarith` 和 `positivity` 强大得多——也就是说，它们可以证明后者无法证明的不等式。理论上，它们可以用于证明以下任何类型的陈述： * 证明一个多项式在全局上是非负的 * 证明一个多项式在一个半代数集上是非负的（即，由一组多项式不等式定义） * 证明一个半代数集是空的，即，一个多项式不等式系统是不可行的 其底层理论基于以下观察：如果一个多项式可以写成其他多项式的平方和，那么它在任何地方都是非负的。证明这种分解存在的定理是 20 世纪实代数几何的里程碑式成就之一，而它与 21 世纪半正定规划的联系使其成为一个实用的计算工具，这也是该软件在后台所做的事情。