最新

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

我日常使用的软件，没有一个是主要由 AI/LLM 编写的。我并没有刻意回避 AI 程序，但也没找到任何有用的。 我说“有用的软件”时，特别指的是我奶奶也能认出来的软件——操作系统、IDE、DAW、DBMS、文字处理软件、3D 建模软件、游戏引擎、视频编辑器、CAD 软件、电子表格应用程序、编译器、浏览器等等。我对那些花哨的 cat/ls 重写程序兴趣不大。 考虑到过去两年产生的代码行数可能比此前二十年还要多，肯定有比平时更多软件我没有注意到。 有没有一些有用的 AI 编写的程序可以让我看看？如果它们能做一些我用电脑做不到的新颖事情，那就更好了。