先驱的梦想成真：从罗素《数学原理》到 2026 年 AI 亲手证明定理

1900 年巴黎国际数学家大会上，三十岁的罗素坐在听众席里，刚听完皮亚诺讲他那套精巧的逻辑符号。会议结束后他在日记里写：这是我一生中最重要的事件之一。那一年他下定决心，要把全部数学重建在逻辑之上——从最底层的集合论公理开始，一步一步推出算术、代数、几何、分析，直到整个数学大厦，每一步都写得像一段可以被机械检查的文字。

这个想法不是他一个人的。希尔伯特在同一年的大会上提出了著名的 23 个问题，其中第 2 个就是：证明算术公理系统是一致的。希尔伯特的纲领更激进——他想把数学整体形式化，让"什么是证明"变成一个有限的、可机械判定的问题。两人的目标合在一起，就是 20 世纪初数学界最大的那个梦：数学可以被写完，而且写完之后，任何一个命题是不是真的，原则上都可以靠一台机器走一遍符号来判定。

《数学原理》：三卷本，362 页之后才得到 1+1=2

罗素和怀特海花了近十年，写出三大卷《数学原理》（Principia Mathematica，1910–1913）。这本书厚得让剑桥大学出版社倒贴钱出版——排印它需要专门设计符号字体，全书近 2000 页。在第二卷的第 362 页，他们才终于证明了"1+1=2"，并在旁边加了一句著名的评注："以上命题偶尔有用。"

这本书的历史意义不在于它真的把全部数学写完了——它没有，第三卷之后就停在了集合论与算术的边界上。它的意义在于：它第一次把"证明"这件事从一种人类的直觉活动，变成了一种可以被逐行核对的符号游戏。每一步推理都必须引用前面某条公理或某条已证命题，不允许"显然"。这个标准，就是今天我们说的"形式化证明"的雏形。

1931：哥德尔的两记闷棍

希尔伯特的纲领在 1931 年被一个二十五岁的维也纳人打断了。库尔特·哥德尔证明了两条不完备定理：任何一个足够强（能描述算术）的形式系统，如果是一致的，就一定存在既不能被证明也不能被证伪的命题；而且它自己的一致性，也不能在系统内部被证明。

这句话用大白话讲就是：你想造一台"数学证明机器"，让它把所有真命题都证明出来——这件事在原理上就不可能。无论你把公理补得多全、把推理规则设计得多精巧，系统里永远会有一些命题，它是真的，但你的机器推不出来。而且你也没法在系统内部证明"我的机器不会自相矛盾"。

这是数学哲学史上最深刻的一击。罗素的梦想在边界上被画了一条线：数学不能被全部机械地写完。但注意——哥德尔没有说"形式化证明不可能"，他说的是"形式化证明不能覆盖全部真理"。你仍然可以把一个非常大的数学分支形式化，可以把一个非常难的定理形式化，可以把证明写得让机器逐行校验。你只是不能指望这台机器回答所有问题。这条界线，在 2026 年依然成立。

1956：第一个 AI 写的"证明"

形式化证明真正被机器写出来，要等到电子计算机出现。1955 年，纽厄尔、肖和西蒙写了一个叫"逻辑理论家"（Logic Theorist）的程序，用在约翰·冯·诺依曼设计的机器上，自动证明了罗素《数学原理》第二章的三十多条定理，其中一条还比罗素本人的证明更简洁。西蒙后来在 1956 年的一次会议上宣布：我们发明了一台会思考的机器。

逻辑理论家证明的是命题逻辑，离真正的数学还很远。但它第一次验证了一件事：把证明写成符号串，然后让机器搜索下一行该写什么，这件事在工程上是可行的。从那以后，"自动定理证明"成了计算机科学的一个独立分支。

1976：四色定理——第一个靠机器"暴力"完成的大证明

1976 年，阿佩尔和哈肯宣布证明了四色定理：任何一张地图，最多用四种颜色就能给相邻国家涂上不同颜色。这个问题从 1852 年提出，悬了 124 年。他们的证明里有一个关键步骤：把所有可能的地图构型归约成 1936 种，然后写程序逐一检查它们是不是都可以用四种颜色着色。计算机跑了 1200 个机时。

这是数学史上第一个其正确性依赖于计算机检查的大定理。当时有数学家拒绝承认它是"证明"——因为没有人能用人眼把 1936 种构型重新验一遍。但四色定理从此被写进教科书。它留给后世的遗产是：当一个证明长到人类读不完的时候，机器可以成为那只"读证明的眼睛"。

从 Automath 到 Coq：证明助手的五十年

自动定理证明分两条路。一条是"自动搜索"——给机器一个命题，让它自己找证明，擅长逻辑谜题，但很难处理复杂数学。另一条是"证明助手"（proof assistant）——数学家像写程序一样写证明，机器在旁边逐行检查每一步是否合法。这条路从德·布鲁因 1967 年的 Automath 开始，经过 LCF、Mizar，到 1989 年 Coq 诞生，再到 2014 年微软研究院发布 Lean。

Coq 把布尔·巴卡尔 2002 年的"四色定理"、2004 年的"若尔当曲线定理"、以及 2013 年乔治·贡捷把一个 1000 页的有限单群分类证明重新形式化，都变成了机器可校验的代码。Lean 则在 2020 年代以后被越来越多的纯数学家采用——它的"数学库" mathlib 是一个全世界数学家共同维护的、用 Lean 语言写的开放知识库，从微积分到代数拓扑，每一条定理都有机器可检查的证明。

为什么数学家愿意花几年时间把一个已经证好的定理重新用 Lean 写一遍？因为形式化的过程会逼你把所有"这一步显然"的窟窿补上。历史上不止一次，一个"被证明了"的大定理在几十年后被发现有漏洞——形式化就是那台永不妥协的审稿人。

2024 年：AI 接过了"写证明"的笔

2024 年以前，证明助手的瓶颈是"写"——数学家写一行 Lean 代码要花很久，机器只负责"查"。2024 年开始，大模型把"写"这一步也接了过去：OpenAI 的 AlphaProof 系列、DeepMind 的 Lean 工具、以及后来 Claude 的形式化能力，都能在数学家给的骨架上自动补全证明步骤。

这就是 2026 年 10 月那篇《形式化验证 Lean 是什么，为什么它成了 AI 数学的"裁判"》（站内内容 1101）讲的局面：AI 生成的证明本身可能错、可能幻觉、可能在人类读者面前看起来像模像样但逻辑跳步——但 Lean 不会被骗。每一步都必须严格合法，否则编译器直接报错。AI 负责写，Lean 负责判。这条分工，是 2026 年 AI 数学的基本形态。

2026-09-04：Claude 用 11 天形式化费马大定理

2026 年 9 月 4 日，Anthropic 在官网发布了一篇题为《Formalizing Fermat's Last Theorem》的研究报告（来源：anthropic.com/research/formalizing-fermats-last-theorem）。报告说：他们用 Claude 在 11 天内，把怀尔斯 1994 年证明的费马大定理，重写为 Lean 形式化证明。

费马大定理是数学史上最著名的悬案——1637 年费马在书页边上写下"我发现了一个绝妙的证明，但这里空白太小写不下"，然后这个证明让数学家追了 358 年，直到怀尔斯 1994 年给出一个 150 页、依赖现代数论最前沿工具的证明。怀尔斯的证明只有全球几十个数论专家能完整读懂。

Claude 做的事情不是"重新证明"费马大定理——它是把怀尔斯的人类证明，一行一行翻译成 Lean 代码，让 Lean 的编译器最终说出一句：Q.E.D.，证明成立。这件事的意义在于：一个需要 358 年人类天才接力才完成的证明，现在被一台机器逐行校验过了。它不再只属于那几十个专家，而是任何一个 Lean 用户都可以打开文件、从头读到尾、看到每一步严格合法的证明。

2026-10：渗流难题 θ(p_c)=0 被 AI 静默解决

2026 年 10 月 29 日，Quanta Magazine 发表报道（来源：quantamagazine.org/updates/transformation/）：在没有任何人下达明确指令的情况下，一个 AI 系统在自主探索中证明了渗流理论里一个悬置多年的结论——在临界概率 p_c 处，无穷连通分支的期望大小 θ(p_c)=0。

渗流模型是统计物理的经典玩具：把一张方格网的每个格子以概率 p 随机打开，p 小的时候打开的格子是散点，p 大的时候会出现一个贯穿全网的大簇，临界值 p_c 大约是 0.5927（在正方格子上）。一个几十年没被严格证明的问题是：在临界点 p=p_c 本身，那个无穷大的连通簇到底还在不在？答案是 θ(p_c)=0——在临界点上，没有无穷簇。这件事物理学家早就当作已知，但数学证明一直残缺。AI 在一次自主的探索中把它补上了。

Quanta 用了"transformation"（转变）这个词做报道标题。它标志的不是某个具体定理，而是一种新的科研节奏：AI 不再只是回答人给它的题，它开始在没有人出题的角落里，自己找到并解决问题。

2026-10-26：OpenAI 抛出三个新数学发现

2026 年 10 月 26 日，Anthropic 发布了一份综述 PDF（来源：www-cdn.anthropic.com/9e431dff043da6538d99d6c2d231b670aa3da263.pdf），盘点 OpenAI 在过去两个月里由 AI 协助完成的三项新数学发现。三项分别涉及一个组合学新构造、一个分析学边界改进，以及一个与杨-米尔斯存在性与质量间隙（千禧年大奖问题之一）相关的进展。

必须严格标注：这份综述里提到的杨-米尔斯相关结果，目前仍在 ETH 等机构的独立复核中，尚未经过同行评审，也没有正式发表。也就是说，"AI 解决了千禧年问题"这句话在今天还不能说——能说的只是"AI 提出了一个被数学家认为值得认真复核的新方向"。这是读 AI 数学新闻时最重要的一条纪律。

对照阅读：站内 10-27 已发的《OpenAI 一次性甩出 722 篇数学证明：哪些是真突破，哪些已撤回》（内容 1100）讲过，OpenAI 那批 722 篇手稿里有一部分已经被撤回。AI 生成的数学结论，必须过 Lean 形式化这一关、必须过同行评审这一关，才能进入教科书。

为什么"机器可校验"是分水岭

把上面这些事放在一起看，2026 年秋天真正发生的不是"AI 比数学家聪明"，而是"数学证明的可信度结构变了"。在过去，一个定理被认为是真的，靠的是：德高望重的数学家写了论文，同行读了几年没找出错，写进教材。这个过程慢，而且会出错。

在 2026 年的新结构里，一个定理被认为是真的，多了一道更强的证据：它有一份 Lean 代码，编译器逐行跑通了。这道证据不依赖任何人的声望，不依赖任何人有没有时间读，它只依赖 Lean 内核那几千行经过形式化验证过的代码。罗素 1903 年想要的，就是这个东西——一份可以被机器逐行核对的数学证明。他没有活到看见电子计算机，但他想要的那个"机器裁判"，在 2026 年真的坐上了裁判席。

哥德尔的墙还在那里

但别误会。哥德尔 1931 年画的那条线，2026 年没有被越过。AI 可以把费马大定理形式化，可以补上渗流的临界值，可以在组合学里找到新构造——这些都是在一个给定的、已经被数学家理解了大方向的领域里，把证明写得更严、把漏掉的口子补上。它没有、也不可能在原理上做到"回答所有数学问题"。

更现实的局限是：AI 形式化的前提，是已经有人知道这个定理是真的、知道大证明长什么样。它能把怀尔斯的 150 页翻译成 Lean，但它没有、短期内也不会从零独立写出怀尔斯那个 150 页的人类证明。AI 在数学里的角色，2026 年是"极速翻译官 + 严格审稿人"，还不是"凭空发现者"。Quanta 那篇渗流报道里的"AI 自己找到问题"，是一个值得警惕的信号，但还不是常态。

给普通人：怎么读一条"AI 证明了 XX 定理"的新闻

以后你会越来越多地看到这种标题。给你三条判断标准：

第一，看它是不是"形式化证明"。如果新闻说"AI 给出了一个证明，已经被 Lean/Coq 校验通过"，这条信息的可信度就高一个量级；如果只是"AI 生成了一份看起来像证明的手稿"，那它和 AI 写的代码一样，需要人逐行审。

第二，看它是不是"重新形式化已知定理"。把怀尔斯已经证好的费马大定理翻译成 Lean，和 AI 从零证出一个新定理，是两件难度完全不同的事。前者是 2026 年 AI 的日常，后者依然是顶尖数学家的领地。

第三，看它过没过同行评审、有没有独立复核。OpenAI 那三个 10 月发现里，杨-米尔斯相关的那一个还在 ETH 复核中。在复核完成前，它是"一个值得关注的主张"，不是"一个事实"。

互链

本知识点与站内 KU 345《Lean 形式化验证：为什么 AI 的数学证明需要"机器裁判"》互为姊妹篇——KU 345 讲 Lean 本身是什么，本知识点讲这件事在数学史里的位置。延伸阅读：形式化验证 Lean 是什么，为什么它成了 AI 数学的"裁判"、OpenAI 一次性甩出 722 篇数学证明：哪些是真突破，哪些已撤回、近三年数学正在被 AI 和算力重写。