最新

目前，Lean 对非线性不等式的支持相当有限。这个软件包旨在解决这个问题。它包含了一系列 Lean4 的策略，用于通过平方和（SOS）分解来证明多项式不等式，并由 Python 后端提供支持。您可以通过 Python 或 Lean 使用它。 这些策略的能力远超 `nlinarith` 和 `positivity`，即它们能够证明这些工具无法证明的不等式。理论上，它们可以用于证明以下类型的陈述： - 证明一个多项式在全局范围内非负 - 证明一个多项式在半代数集合上非负（即由一组多项式不等式定义） - 证明一个半代数集合为空，即证明一个多项式不等式系统是不可行的 其基础理论基于以下观察：如果一个多项式可以表示为其他多项式的平方和，那么它在任何地方都是非负的。证明此类分解存在性的定理是20世纪实代数几何的标志性成就之一，而它与21世纪半正定规划的联系使其成为一种实用的计算工具，这正是该软件在后台所做的工作。