数学从此彻底改变——Kevin Hartnett

摘要

• AI 数学正沿着形式化与自然语言两条路径推进。 Hartnett 对比了 AlphaProof 在 2024 年 IMO 上凭借 Lean 和大量算力取得的银牌水平成绩，以及 Google DeepMind 和 OpenAI 在 2025 年 7 月公布的、以自然语言作答的金牌水平成绩。模型生成大量候选证明时，Lean 仍能提供有价值的训练和筛选机制：“Lean 能告诉你哪些证明是对的。”
• 形式化的成本相对其预期收益过高，一直是采用门槛。 Hales 花了 20 人年形式化 Kepler 猜想；de Bruijn 因子意味着每行非形式化文本往往要写 20 行或更多形式化代码。数学家最想做的是“发现新数学”，因此自动化和加深理解，比单靠确保正确性更能推动采用。
• 自动形式化把稀缺精力转向了数学库的设计与维护。 AI 将论文转成 Lean 的速度远快于人类团队，但经过检验的代码仍可能使用繁琐的定义和薄弱的抽象。Hartnett 称这股涌入“有点像特洛伊木马”；Buzzard 预计 AI 生成的数学库会越来越大，同时坚持 mathlib 必须守住概念质量。
• 机器验证把信任问题向上游推到了定义和规格说明。 Buzzard 的团队形式化了 50 条 Annals 定理陈述，随后用 AI 找出翻译错误，以及涉及 4 位菲尔兹奖得主的已发表定理陈述中遗漏的假设。这些案例里，专家理解作者本意，但照字面写出的陈述并不成立：“显然，n 必须至少是 3。”
• 形式化既能加深理解，也能推动新发现。 检查 Scholze 的 6 页论证，带来了概念上的简化，也化解了他对无人仔细读过该论证的担忧：“终于真的有人读过它了。”另一次合作中，Tao 把 2,200 万个蕴含关系问题缩减到只剩 4 个未解案例，同时发现了此前陌生的数学构造。
• AI 代码验证可能成为应用方向，但前提是行为规格写对。 压缩程序只要原样返回输入，就能满足往返证明；证明正确，并不代表压缩有用。Avigad 提到 Harmonic 看好数学证明能力迁移到软件验证的可能性，而 Buzzard 对结果仍持保留态度：“最后能不能成，我不知道。”

精读

1. 一个证明可以解决问题，却仍令同行评审无从下手

• Scarfe 从 Kepler 猜想讲起：橘子堆成金字塔的排列看起来最密，密度约为 0.74。Thomas Hales 和 Samuel Ferguson 把问题化约为一系列构型；Hales 最终写出 1,767 个计算机程序，随着构型密度逼近上限，验证难度也不断上升。1998 年夏天，计算工作告一段落，但别人如何核验整套结果，仍是个问题。

• Hartnett 描述了 Annals of Mathematics 面对的局面：庞大的计算藏在代码里。审稿人检查过的部分看起来都正确，却无法确认整个结构如何彼此衔接。De Moura 回忆，论文获接收时附有免责声明，表示大约有 99% 的把握。此后，Hales 用 HOL Light 和 Isabelle 形式化了这一结果；那时 Lean 尚未出现。

• Hartnett 强调，合法性与数学上的生发能力是两回事。Hales 解决了问题，但他采用的计算方法相对基础，并未像 Wiles 证明 Fermat 大定理那样催生广泛有用的概念。Lessard 想要的不只是可靠答案：“我想知道它为什么会得出某个答案，我想知道其中的理由。”

• 经济账解释了人们为何抗拒：Hales 为形式化投入了 20 人年，而 de Bruijn 因子通常意味着每行非形式化文本要对应 20 行形式化代码，甚至更多。对确信结果正确的数学家来说，这份额外保障可能不如新发现有价值。日常核验在很大程度上仍依赖社群信任，以及对既有数学的熟悉程度。

2. Lean 把信任集中在一个小型内核上

• Hartnett 回顾 de Moura 早年的成功：2006 年前后，微软内部定理证明项目重复投入，他因此启动了 Z3。Z3 能表示软件的执行路径，并排除那些对应特定漏洞的变量组合。Hartnett 说，Z3 为微软节省了数亿美元，也赢得了自动定理证明竞赛；但表达能力有限，令 de Moura 并不满足。

• Lean 把编程语言和交互式证明助手结合起来；它本身也是用 Lean 实现的。用户可以编写程序、陈述性质并构造数学证明。逻辑基础决定陈述的含义，名为 kernel 的检查器则核验推导过程。De Moura 对信任范围的表述刻意收窄：“我们只信任 kernel。”

• 这条边界很重要，因为 Lean 整体“有无数个 bug”。kernel 接受一个错误陈述，远比拒绝一个正确陈述严重：错误可能沿着后续证明不断传播。本期提到 Agda、Coq 和 Isabelle 的 kernel 都曾出现 bug。受 HOL Light 影响，de Moura 倾向于采用精简的 kernel，让独立实现也能检查证明证书。

3. 数学用户在基础设计之争中占了上风

• Avigad 曾大量使用 Isabelle，也称赞它的自动化能力，但他发现，简单类型论难以处理现代数学中彼此交织的代数结构。自己使用 Rocq 工作 1 年后，他得出结论：依赖类型论更适合这类数学。另一方面，de Moura 说，他在 2009 年和 2010 年用了 1 个休假年，研究如何形式化 Feit–Thompson 定理。

• Avigad 承认这种设计需要权衡：“能力越强，责任越大。”依赖类型论带来了实现难度、易用性问题和边界情况。2013 年夏天，de Moura 选择了依赖类型论，这让 Avigad 相信 Lean 有望用于重要的抽象数学。

• De Moura 说，这份额外投入的回报不止于纯数学。密码学和差分隐私同样需要强大的数学库。他的前同事 Cédric Fournet 后来告诉他，mathlib 提供了“我验证密码学所需要的恰当抽象”。支持要求严苛的数学用户，也帮助 Lean 为最初瞄准的软件验证用户构建了有用的抽象。

4. 共享数学库让 Lean 不再只是基础演示工具

• Buzzard 投身其中，起因是一场研究危机。他养育 3 个孩子后重回高难度数学，发现 p-adic Langlands 纲领相关文献中有不少缺口和错误。他批评的是建立在 Scholze 发现之上的研究，并非 Scholze 本人的严谨工作。缺少能用现实检验的具体应用，他担心未经核验的抽象会堆成“纸牌屋”。

• 早期 mathlib 只有约 3 万行代码，内容是基础的本科数学；实数刚刚加入，复数则尚未纳入。Buzzard 把复数补了进去——“复数版权归 Kevin Buzzard，2017 年”——随后招募本科生形式化他们正在学习的内容。大约 3 年后，这个数学库已经涵盖了他们本科课程中的大部分内容。

• Hartnett 将这种协作氛围称为“大家一起搭谷仓”，Commelin、Massot、Avigad、Carneiro、Buzzard 等人都参与其中。De Moura 把 Commelin 的大型项目比作软件工程：架构师把工作拆成小块，让原本不认识的合作者、甚至高中生也能完成。机器检查免去了手动核验每位贡献者的证明是否正确。

• Tactic 减轻了形式化中的重复劳动。Hartnett 回忆，早期形式化甚至连看似显然的算术都不容易；辅助程序可以自动处理反复出现的论证，同时生成供 Lean 检查的证明。例如，ring tactic 会构造代数恒等式的证明，直到 Lean 报出“没有目标”。De Moura 还让用户能够自己编写 tactic，使社群可以不断扩展 Lean 的能力。

5. 形式化定理陈述，让数学家以更低成本触及前沿

• Buzzard 起初希望通过形式化概形证明 Lean 的价值，但数学家认为这些内容已经过时几十年。2018 年前后，Buzzard、Massot 和 Commelin 转而瞄准 Scholze 的 perfectoid spaces，着手构造表达它们所需的定义。Hartnett 将其称为“通往前沿的一座窄摩天楼”：mathlib 广泛覆盖的范围大约到研究生一年级数学，中间仍有一些本科内容的缺口，但也在个别领域深入得多。

• Hales 提出一条成本更低的路径：不必把完整证明全部翻译出来，可以先形式化定理陈述。Buzzard 举例说明其意义：第 3 节可能已经证明素数 p 至少是 5，但第 7 节的定理只提到 p。读者如果直接从第 7 节开始，可能会漏掉前面继承下来的假设，误解究竟证明了什么。

• Buzzard 起初就意识到，全面检查现代论文不现实，但定义对象、陈述主张似乎可行。Hales 在 2017 年推动了这个想法；7 年后，Buzzard 写下申请这项工作的基金提案。经过 1 年，团队完成了所选近期顶级期刊定理陈述的约 20%；他预计接下来 1 年会有大幅进展。

6. Scholze 那篇无人读过的论证带来了突破

• 2020 年 11 月，Scholze 问 Buzzard 是否仔细读过一篇近期预印本。伦敦一个读书小组为此花了 1 个学期，但后续提问暴露出问题：他们只是略读了一段 6 页的技术证明，可能是定理 8.4。Scholze 从 Princeton 和 Harvard 得到的回答也差不多：“大家都是这么说的。”

• Scholze 和合作者 Dustin Clausen 相信论证成立，但 Scholze 担心没人认真核查过它。由于其中不少技术内容最终属于本科数学，Lean 可能足以验证。社群一开始预计要花 1 年；Commelin 找到了简化方法，关键论证在 6 个月内完成了检查。

• 这项成果带来的不只是安心。Buzzard 回忆，Scholze 很兴奋，因为形式化揭示了一个更具概念性的论证，也让他觉得“终于真的有人读过它了”（“something has now actually finally read it”）。Avigad 将这一价值与思考数学“API”联系起来：概念如何打包、哪些信息对外开放，以及独立开发的组件如何交互。

• 曝光度提升后，职业数学家开始关注 Lean，最先问的往往是它能否处理自己最新的定理。答案通常还是不能，但他们可以先用 Lean 搭建各自领域的基础。COVID 也加快了参与：形式化既有吸引人的数学内容，又像电脑游戏；交互式证明还允许研究者进行静态 PDF 做不到的探索。

7. AI 的进展正在超出单一验证架构的能力

• Hartnett 解释了数学为何适合 AI 训练：清晰的正确性信号有助于强化学习。但 AlphaProof 需要 Lean 格式的题目，竞赛题却以自然语言给出。据报，DeepMind 几乎完美地把代数和数论题目自动形式化，覆盖率约为 80%；像故事题那样的组合数学则更难。由此形成的训练题库达到数千万道形式化问题。

• 参加 2024 年 IMO 时，AlphaProof 在人类竞赛结束后才拿到题目，使用了更多时间和海量算力，得分达到银牌水平。无论强化学习还是解题竞赛，Lean 都负责验证。比较成绩时，既要承认这项成果，也要看到资源条件并不对等；这并非一次与人类考生完全相同的考试。

• 2025 年 7 月，Google DeepMind 和 OpenAI 报告了以自然语言证明取得的 IMO 金牌水平成绩。Google 的结果由 IMO 正式评分；OpenAI 的成绩则另行评估。两者都没有依靠 Lean 验证答案。尽管如此，Hartnett 预计两条路径都会继续发展：表达能力强的模型负责生成论证，Lean 则能快速筛选大量候选证明。

• 本期在 2026 年 9 月的更新中提到，Epoch AI 的固定预算测试里，一个尚未发布的 OpenAI 模型用 Lean 证明了 Erdős 问题 126，并通过反例推翻了问题 74：68 道题中解决了 2 道，其他 4 个模型一道也没解决。本期还提到，OpenAI 于 9 月 8 日声称用 Lean 解决了 Navier–Stokes 千禧年大奖难题，“条件并不理想”（“not under the best circumstances”）；但这件事不在本期讨论范围内。

8. 穷举探索能发现陌生的数学

• Tao 在 2024 年 9 月启动 Equational Theories，利用 Lean 检查代数定律之间的蕴含关系。不到 1 个月，2,200 万个问题就缩减到 238 个；到 11 月下旬，剩下 138 个。3 月底时，仍有 4 个问题已经好几周没有进展。不过，解决所有蕴含关系从来不是项目的唯一目标。

• Tao 想象一种类似现代物理学的实验数学分支：大型协作和海量数据与理论相互补充。探索过程中，团队发现了 magma 上同调等构造。John Baez 起初称这个项目是“巨大的时间浪费”，后来承认自己从未见过这种构造。对 Tao 来说，这是发现“火星来的数学”的证据。

• Hartnett 还讲到一次带有推测性质的讨论：3 位数学家谈到从公理出发、以 AlphaZero 式方法启动 AI。他们预计，这种方法未必能在偏离人类数学之前，重新发现超出有理数的内容。原因在于抽象方式：人类研究者会选择让人觉得优美、有用且能拓展的概念，而以正确性为目标的搜索不必遵循这些偏好。

9. 自动形式化带来新的维护瓶颈

• AI 有望降低 Hartnett 指出的两道门槛：学习 Lean 繁琐的语法，以及手动扩充数学库。智能体编程可以帮助数学家表达证明，而不必掌握语言的每个细节。更进一步，自动形式化承诺能把整本教科书转成 Lean；Hartnett 说，如今把论文转成 Lean 代码，所需时间只相当于过去人类团队的一小部分。

• 难点在于数学库的规范质量。Mathlib 追求“打磨成熟的数学”：概念要经过充分理解，抽象层次要适合后续工作。改动一个基础定义，就可能让数千个文件出错。因此，涌入一批形式上有效、但表达别扭的材料，会增加审核和整合工作，并不会自动丰富共享数学库。

• Buzzard 观察到，AI 很乐于“直接一路蛮干”，完成那些人类会重新设计的构造。基础定义变化造成下游代码出错时，AI 也可能负责修复。他预计，1 年内就会出现 AI 开发的数学库，但按这些标准衡量，它们的设计会考虑得更不周全。Mathlib 的维护者仍然要求概念质量；单纯往问题里灌 token，解决不了双方目标的差异。

10. 证明经检验后，信任问题转移到定义上游

• Scarfe 直接指出了边界：“经检查的证明仍然可能证明了错误的东西。”必须有人确认形式化猜想是否准确表达了预期定义和假设。Kernel 检查推导过程，却不会认证人类选择的目标是否正确。“信任基本上已经转移到了上游。”

• Buzzard 的团队翻译了 50 条 Annals 定理陈述，并在发表前让 AI 检查。AI 找出了团队的翻译错误，也发现有些陈述忠实复现了已发表文本中的缺陷。涉及 4 位菲尔兹奖得主的定理陈述，字面上都不成立，因为遗漏了 n 至少为 3、集合非空等假设。

• Buzzard 说，自己的看法变了：几年前，他会认为专家写下的内容就是他们的本意。如今他看到，形式化揭示了专家理解与字面表述之间的落差。他所说的“从 99% 到 100%”，指的是把这些隐含条件明确写出，而不是宣称原本想表达的结果已被推翻。

• Scholze 的疑问更深一层：人们怎么知道 Lean 中的定义与预期的数学对象一致？“数学仍然是一项人类活动。”Commelin 和 Topaz 提供了具体例子作为单元测试——那些看起来像鸭子、叫起来也像鸭子的对象。它们算不上无懈可击的证据，但 Commelin 认为，至少不比阅读传统定义让人更不放心。

11. 软件验证的效果取决于目标设定是否到位

• Scarfe 提到 Kim Morrison 的实验：用 Claude 智能体在 Lean 中实现 zlib。De Moura 说，AI 翻译了 C 代码，反复修复实现直到通过 C 版本的测试套件，并证明对任意数据和压缩级别，压缩后再解压都能恢复原始输入。

• Scarfe 用盲人摸象比喻不完整的规格说明。De Moura 给出最直接的失败案例：压缩和解压函数都设为恒等函数，也满足往返性质，却完全没有压缩。补充约束或许可以要求检查输出大小，并在测试案例中与 Rust 实现的压缩结果对比。

• De Moura 区分了人类检查代码时由 AI 提供协助，与让 AI 不经检查地“放手去做”。后一种情况下，不完整的规格说明可能让 AI 精确满足字面要求，却漏掉真正想要的行为。Hartnett 也提到，有人怀疑规格说明能否充分覆盖大多数真实程序那样复杂的软件。

• Scarfe 认为，审查和验证是智能体编程目前的瓶颈。Avigad 认为 AI 或许既能写实现，也能写规格说明，从而让形式化验证发挥更大作用；他还提到，Harmonic 相信数学证明能力可以迁移到软件验证。Buzzard 对结果仍持开放态度：“最后能不能成，我不知道。”

12. 基础设施仍然是人类的事业

• Hartnett 描述了约 2018 至 2022 年间的一次明显分裂：de Moura 退出日常协作，转而构建 Lean 4，mathlib 则继续发展。他没有工程团队支持，还要应对不断涌来的用户请求。他与 Carneiro 的摩擦，源自双方对 Lean 及其开源数学库的不同愿景。De Moura 抱怨，随口提出的想法会让接收者承担越来越沉重的反驳成本。

• Hartnett 通过 6 到 7 份核心材料、私人邮件，以及公开和私下的 Zulip 对话，还原这段历史。Buzzard 说，当参与者意识到 Hartnett 并非想找反派或挖丑闻时，信任才逐渐建立起来。他自己的讲述以重归于好收尾：一个下午，他和 de Moura 在 Seattle 散步，聊 Lean，也聊 Lean 之外的生活。

• Buzzard 说，面对从“悲伤”到兴奋不等的反应，自己属于兴奋的那一端，但没人知道 AI 数学最终能发展到什么程度。他预计定理和理解都会增加。最后，他给出另一面：“让我们的目标变得特别的，是这些目标属于我们。”关键仍在于，人类想如何与机器互动，又想理解什么。