Lean：正在重写数学的编程语言
B座17楼 ｜ B座17楼公众号 ｜ 2026-09-26

Lean：正在重写数学的编程语言

它将数学证明转化为机器可检查的代码，并正成为AI时代最大数学主张背后的验证层。

Vagelis Plevris

2026年9月8日，OpenAI宣布了一件非同寻常的事。

一个内部AI系统提出了纳维-斯托克斯方程存在性与光滑性问题的拟解决方案——这是七个千禧年大奖难题之一。

但在数学论文之外，OpenAI还发布了另一样东西：

一份用Lean写成的证明。

对大多数人来说，甚至对许多数学家来说，这个名字几乎没有什么意义。Lean不是一个著名的定理，不是一个AI模型，也不是像Mathematica那样的计算机代数系统。

Lean定理证明器的标志。Lean是一种交互式定理证明器和函数式编程语言，用于形式化并用机器检查数学证明。

点 击 图 片 看 原 图

图片来源：Lean，2014，通过Wikimedia Commons公共领域。

它是一种编程语言。

更准确地说，它既是编程语言，也是证明助手：一个系统，可以在其中用形式语言写出数学定义、定理和证明，并由计算机检查。

这一区别可能变得极其重要。