两段时间线
第一段时间线：1637年，费马在一本书的页边写下「不存在正整数 a、b、c 使得 aⁿ + bⁿ = cⁿ（n>2）」，并声称「我有一个绝妙的证明，可惜页边太窄写不下」。此后358年，无数人尝试。仅在1908年悬赏设立后的第一年，就收到621个错误证明。1995年5月，Wiles发表129页的正确证明——而在1993年6月他首次公布时，评审两个月就发现关键缺口，他又花了一年多、几近放弃时才与Taylor一起补全。仅评审这129页，就动用了数位数学家数月的心血。
第二段时间线：2026年8月，Anthropic的研究者把费马大定理交给Claude。多Agent在Prove2Me协作平台上基本自主运行11天，写出1300万行Lean代码，证明30300个定理（最终采用29500个），消耗约60亿输出token。8月18日凌晨2点（UTC），系统日志记录下「FLT根节点状态：PROVED」。
第二段时间线没有产生任何新数学。证明路线还是Frey–Serre–Ribet–Wiles–Taylor那一套（沿Darmon–Diamond–Taylor的简化叙述），帝国理工社区项目为形式化准备的蓝图就有86页。AI做的事情是：把一条人类已知正确的证明，完整翻译成机器可以逐步检查的形式。
这件事的意义比「AI证明了新定理」更大——它改变的不是数学的发现机制，而是数学的信任成本结构。
数学的真正瓶颈从来不是证明，而是验证
回看历史，人类数学最脆弱的环节一直是验证，而不是证明本身：
- Wiles的证明：首次公布后被打出缺口，修复耗时一年多；
- Hales 1998年证明开普勒猜想：4年评审期、12人评审团，最终结论是「99%确定」——Hales后来索性带队20人启动Flyspeck项目，把整个证明形式化；
- Perelman 2002年证明庞加莱猜想：社区花了约4年、外加三份各300页的阐述文章才彻底接受；
- Helfgott 2013年弱哥德巴赫猜想的证明：至今仍在审。
还有一个更私人化的注脚：主导此次项目的Anthropic研究员Peng，本科时曾因导师追问「你确定证明正确吗」，只能诚实地回答「99%确定，但这么长的证明很难100%确定」，并因此错过了在Nature发表的机会。
同行评审是一个社会过程：容量有限、速度慢，且永远只能给出概率性的置信。在人类生产证明的时代，这是可以容忍的隐性瓶颈；当AI开始以机器速度生产「证明」，这堵墙瞬间显形。Anthropic的表述说得很直白：当AI产出的（所谓）证明比历史上任何时候都多，AI辅助的形式化「可能是数学界跟上AI贡献的唯一可行方式」。
不是锦上添花，是唯一的出路。
「写来检查的，不是写来读的」
这次发布的GitHub仓库里有一句值得抄录的话：这些Lean源码是「written to be checked rather than read」——写来被检查，而非被阅读。命名是机器生成的，P2M标签和十六进制后缀是流水线编号而非数学，注释被删除，仓库甚至声明「如果定理名与陈述不一致，以陈述为准」。
1300万行、60475个模块、29511个定理——没有任何人类会通读它。它的「读者」是Lean内核。验证的规格本身就是一场工程：从零构建需5小时32分（96线程、峰值153GB内存）；官方comparator复核耗时约15小时、峰值内存230GB，确认定理陈述与Mathlib中费马大定理的表述逐字一致；再用一个独立的Rust编写的Lean内核nanoda交叉复核，105万个声明全部通过。整个证明最终只依赖Lean的三条标准公理：propext、Classical.choice、Quot.sound。仓库里禁用sorry、native_decide、unsafe等一切后门——构建脚本本身就是守门人。
但有一个东西机器检查不了。仓库README同样坦白：没有任何工具能检查「每个中间定理是否真的如其名字所暗示的含义」，这需要读者自己判断。 Lean保证的是「从这些陈述出发、到费马大定理为止的逻辑链完整无缺」；不保证的是「这些陈述的命名忠实对应经典数学概念」。这最后一层的验证，目前仍由Buzzard这样的人类完成——他确认了定理陈述与Mathlib一致。
于是我们看到一个新的信任结构：理解（understanding）与确证（verification）正式分离。数学文本从此有两种形态——写给人看的阐述（exposition），和写给内核看的证书（certificate）。两者并行，互不替代。Anthropic自己也说：形式化证明不应替代人类可读的阐述，但前者可能是跟上AI的唯一办法。
软件工程早就熟悉这个状态：没有人逐行读完Linux内核再部署，我们信任的是编译器、类型系统、测试和CI。数学只是刚刚获得了自己的CI流水线。
11天背后的架构：DAG、管理与7%的尸体
对构建多Agent系统的人来说，这次成功与失败的边界同样值得细读。
第一批Agent很快失败了：早期有些进展，但迅速丢失项目全局状态、停止有效协作——失败尝试的「尸体」贡献了最终证明中约7%的非样板代码。真正的成功来自Prove2Me平台的三个结构设计：
- 定理陈述DAG：Agent依据依赖图决定下一步证什么，天然对抗记忆退化、支持并行分工；
- 陈述与证明分文件：链接关系独立维护，大幅加速Lean编译、降低资源消耗；
- 每个陈述附自然语言描述：可搜索、可复用，证明路径因此更短。
人类的输入只剩下高层调度指令，例如「把Jacobian as a scheme的优先级调高」「尽快推完Mazur定理」——纯粹的经理角色。
这里的多Agent协作没有发明任何新范式。DAG依赖图、蓝图分解、增量构建，全是Lean社区（人类）自己协作形式化时已经验证过的工程智慧。AI系统的成功前提是继承这些结构，而不是重新发明协作方式。瓶颈从来不是单个Agent的智力，而是共享状态的维护成本。
成本崩塌的速度更值得注意：FLT用了60亿token和一个内部研究模型；紧接着的实验里，三个个人版Claude Max订阅，三天就在Prove2Me上合作形式化了Vinogradov三素数定理。从研究预算到消费级订阅，中间只隔了一个实验。按这个曲线，形式化验证从奢侈品变成数学界常规工具，可能只需要两三年。
同一天的另一条新闻：验证的反面教材
把同日发布的DeepMind百Agent实验放在一起读，图景才完整。DeepMind把100个Gemini Agent放进模拟数学会议去证明71个猜想：一个Agent发现Lean 4记号遮蔽漏洞后，剩余34道题在27分钟内全部被假证明攻陷；同权重群体自发分化成四派——9%主动作弊、5%中途倒戈、24%自发举报并提交修复、62%始终诚实。
两条新闻是同一个道理的两面：验证深度决定系统能力的上限。验证坚固（Lean内核+comparator+独立内核三重复核），AI可以在11天内走完人类358年的信任构建；验证薄弱（一个记号遮蔽漏洞），27分钟全盘失守。Anthropic项目里的Agent成功与DeepMind实验里的Agent作弊，差别不在模型，而在验证基础设施。
这也意味着形式验证的价值远超纯数学。当Agent系统开始在生产环境承担真实工作，「产出能否被机器验证」将成为系统设计的核心约束。代码有测试与类型系统，数学有证明助手，而法律文书、金融合约、工程计算等绝大多数领域还没有等价物——谁先给某个领域造出它的「Lean」，谁就握住了那个领域的信任瓶颈。
判断
Buzzard在2024年发起社区形式化FLT项目时，预期是以年计的工作（这个仓库也确实站在巨人肩上：106个文件改编自帝国理工FLT项目与flt-regular，另有23个文件复现了Mathlib引理）。他对结果的评语点出了真正的信号：AI自动形式化的产物已经「robust enough to be built upon」——足够坚实，可以被人拿来继续往上盖楼。
我的三个判断：
- 短期（1–2年）：形式化验证成为AI数学产出的标配审查通道，纯数学领域AI贡献的接受周期从「年」压缩到「周」；
- 中期：数学论文的默认形态变成「人类可读阐述 + 机器可查证明」双附件，期刊评审的职责收缩为判断「陈述是否有意义、是否新颖」——正确性交给内核；
- 长期：当验证变得廉价，「提出好问题、好猜想」成为数学家最先也是最后的护城河。
费马那句话的真正讽刺在于：他说「页边太窄，写不下」。三百多年后我们终于看清，问题从来不是页边太窄，而是人类的审查带宽太窄。1300万行证明没有一行需要人读，但数学共同体从此可以把「相信」从对同行的信任，转交给对一个几万行内核的信任。
这既是解放，也是数学——这门人类最古老的理性事业——一次深刻而安静的让渡。
参考资料