Anthropic官宣了一件挺唬人的事:Claude用11天、基本自主地在Lean证明助手里写出了费马大定理(FLT)的首个端到端、可计算机验证的证明。过程中它写了1300万行Lean代码,证明了29500个中间定理(候选总数30300个),代码规模是数学界最大公共证明库Mathlib的五倍以上。这份证明被送到了Imperial College London的Kevin Buzzard手里,他公开评价这是"extraordinary achievement"。

但翻开证明仓库自己的说明文件会看到一个数字:106个文件的内容,直接取自或改编自Buzzard团队自己的Imperial FLT项目,以及更早的flt-regular项目。这不是从零写出来的证明,是一次站在别人已经搭好的地基上的高速拼装。

350年的证明,20年的"翻译"

费马1637年在书页边缘写下这个猜想,附了句著名的空头支票:"我发现了一个真正美妙的证明,可惜这里空白太小写不下。"350多年里,无数人栽在这句话上。

Andrew Wiles 1995年给出人类第一个证明,129页,期间还有过一次惊魂——1993年公开演讲两个月后,审稿人指出一个致命漏洞,Wiles花了一年多才补上。证明本身就是脆弱的,一环断了,后面全塌。

2005年荷兰计算机科学家Jan Bergstra提出把这个证明"形式化":重写成计算机能逐字核验的形式。人写的证明会跳过"显然"的步骤,Lean不行,它要看到每一步。2024年Kevin Buzzard在Imperial启动社区项目系统推进这件事,光是初期蓝图就有86页,业内预期整体形式化要花数年。

三层验证,和它查不出的东西

内核能证明逻辑闭环,证不了你写的东西是不是你想说的那件事。

Claude的证明经过了三重独立检查:Lean自身内核只用三条标准公理跑逻辑;Nanoda是一个用Rust独立实现的Lean内核,对导出后的证明再核验一遍,防的是Lean自己代码库里可能藏的系统性错误;最后由comparator比对,确认最终定理陈述和Mathlib自带的FLT标准表述完全一致。

这套组合拳比一般同行评审严谨得多。但仓库文档自己也承认一处硬伤:内核能验证逻辑推导是否成立,验证不了定理的名字和自动生成的英文描述,是不是真的对应人类原本想表达的数学含义。1300万行代码,没有人能逐行读完,信任最后落在"内核通过"这四个字上——这已经不完全是数学问题,更接近工程可审计性问题。

  • 风险.命名和描述的语义正确性,是这套验证链条唯一没堵上的口子,也是外部审查最该盯的地方。

"自主"两个字,边界在哪

回到那106个文件。Anthropic的表述是Claude"largely autonomously"完成证明,Buzzard的评价也很正面,但这两件事和"从零证明"不是一回事。

对照一下时间线:2024年10月,已经有团队用Lean单独形式化了FLT里"正规素数"这一特殊情形的证明,走的是更早的Hilbert 90-94路线,只覆盖部分指数。截至2025年5月,Buzzard自述在Imperial的项目已投入约六个月官方精力、约一年非官方精力,并拿到了英国工程与自然科学研究理事会一笔延续到2029年的五年期资助,走的是现代版的Frey–Ribet–Taylor–Wiles路线。

也就是说,Claude没有从一片空地起步。它是在Buzzard团队已经耕耘了一年多、把关键基础设施和部分子定理都搭好之后,用11天完成了最后那段冲刺式的拼装、扩展和组网。这是很不一样的两件事:一个是打地基,一个是在地基上快速起楼。

这不意味着Buzzard的项目被超越或作废。他自己想做的是一套可复用的现代数论形式化基础设施,不是抢一个"最快证明"的名次,Claude的工作反而证明了这套基础设施是能被立刻拿来用的——这是对项目价值的确认,不是替代。

真正被改变的,是验证的速度

比数字更值得记的,是Anthropic提到的另一个小实验:用三个个人版Claude订阅,协作三天就形式化了Vinogradov三素数定理。这说明大规模协作形式化不再是只有大团队、大预算才玩得起的事。

  • 结论.如果重大证明的形式化验证能从"数年"压到"天",数学期刊的评审逻辑迟早要跟着变——机器验证可能会先于人工评审,成为判断一篇论文是否可信的第一道门槛。

对数学圈来说,这才是这次事件真正的分水岭:不是又一个难题被AI攻克,而是"证明是否可信"这件事,开始有了一条比人工评审快得多的替代路径。至于这条路径本身够不够可靠,取决于Nanoda和comparator这类工具能不能持续经受住独立审查——目前还看不到第三方大规模复现这1300万行代码的结果。

数学史上从来不缺"我证明了,但没人信"的故事。Fermat自己那句边注,最后被公认是错的。Claude这次的不同之处在于,它把"信不信"的问题从纯人工判断,变成了半机器可审计的问题——这一步比证明本身更值得记住。