Lean 形式化验证：为什么 AI 的数学证明需要"机器裁判"

2026 年 10 月，OpenAI 一次性公开 722 篇由内部模型生成的数学手稿，但外界很快发现：其中只有约 162 篇附用了 Lean 做的形式化验证。换句话说，真正经过"机器裁判"盖章的，不到四分之一。

什么是形式化验证

形式化验证指把数学命题和证明翻译成一种严格的形式语言，交给计算机逐行检查每一步推理是否符合逻辑规则。传统论文靠同行阅读来"相信"，形式化则靠机器"验算"——只要编译器通过，逻辑链条就不存在跳步。

为什么它突然重要

当 AI 能在几小时内堆出几百页推导，人类审稿人根本读不过来。斯坦福科技评论统计，OpenAI 那批手稿里，10 月 3 日至 6 日新增的 143 篇没有任何一份做了形式化验证。一旦生成端快、验证端慢，数学就会陷入"证明消化不良"——结论很多，可信的很少。

三种角色正在分工

图1：生成者、验证者、消化者三种角色分工——前两者被 AI 加速，消化仍靠人。

• 生成者：AI 提出猜想、构造反例、写初稿。
• 验证者：Lean 等工具把证明转成可机器核对的代码。
• 消化者：人类数学家理解、简化、写成能教给学生的表述。

前两者正被 AI 加速，最后一项仍只能靠人。这场分工，正是今天数学界争论的核心。

---