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

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

Vagelis Plevris

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

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

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

一份用Lean写成的证明。

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

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

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

它是一种编程语言。

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

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

人工智能可以生成一页页令人信服的数学推理。它可以建议引理、操作方程、搜索可能性，并提出人类此前从未考虑过的论证。

但令人信服并不等于正确。

Lean提供的是不同的东西。给它一份完全形式化的数学证明，它就能检查每一步逻辑是否从前一步推出。

没有诉诸权威。没有审稿人说“这看起来是对的”。没有语言模型自信地写下“因此，显然……”

证明要么通过检查，要么不通过。

而这个相对冷门的想法，正开始改变数学的做方式。

Lean究竟是什么？

Lean是一种函数式编程语言和交互式定理证明器。

它主要由计算机科学家莱昂纳多·德·莫拉Leonardo de Moura在微软研究院工作时创建，并于2013年首次以开源软件发布。

莱昂纳多·德·莫拉在ETAPS 2026上关于Lean的演讲。德·莫拉是Lean定理证明器的主要创造者。照片由David Monniaux拍摄，2026年4月13日，通过Wikimedia Commons，采用CC BY-SA 4.0许可。

在Lean之前已有几个证明助手，包括Coq（现称Rocq）、Isabelle和Mizar。它们的核心思想相似。

你不再只在普通数学散文中写证明，而是把定义、假设、陈述和逻辑步骤翻译成精确的形式语言。计算机随后可以验证证明。

Lean基于依赖类型理论——一种类型可以依赖值的数学基础。其下有一个小而受信任的内核，负责检查所谓的证明是否有效。

这个描述听起来令人生畏，但基本想法更容易理解。

假设一位数学家写道：对每一个自然数n，

人类读者立刻理解这是什么意思。

计算机则不然。在机器能够验证陈述之前，每一种成分都必须有精确的含义。

什么是自然数？

什么是加法？

相等意味着什么？

“对每一个”意味着什么？

什么算有效的证明？

Lean迫使这些问题被明确回答。

一旦回答了，机器就能检查随之而来的东西。

数学开始看起来像代码

然后是它的数学陈述：

在最简单的层面上，它告诉Lean某物等于它自己。

没有人需要一个复杂的证明助手来确立2 = 2。

但有趣的事情发生了。

计算机没有测试几个数值例子。它没有估计任何东西。它检查了一个证明。

而检查2 = 2的同一逻辑框架，原则上可以检查由数百万行组成的证明。

目标始终在你面前

换句话说，如果P和Q都为真，证明Q和P都为真。

Lean现在呈现一个目标。

从概念上说，它在说：这是你所知道的。现在证明这个。

你可以把h看作包含合取的两部分：

h.right给出Q的证明

h.left给出P的证明

从假设h中，我们提取Q的证明，然后是P的证明。