费马大定理（Fermat’s Last Theorem，FLT）就是一个典型的例证。费马在一本书的页边写下了这条定理的表述，并附上一句引人遐想的批注：
350多年来，一代代数学家为寻找FLT的证明呕心沥血，无论其证明是否绝妙。1908年，有人宣布悬赏10万德国金马克（相当于今天的100万至200万美元），奖励任何能给出正确证明的人，仅第一年就收到了621份错误的尝试。
1993年6月，Wiles在为期三天的系列讲座中展示了他认为是首个正确的FLT证明。在数位数学家高强度的验证工作进行到两个月时，一位审阅者向Wiles提出了一个问题，暴露出证明中的一个关键漏洞。Wiles花了一年时间试图修补，起初独自进行，后来与他昔日的学生Richard Taylor合作。就在他几乎要放弃这个项目之际，他终于意识到自己早先舍弃的一个思路可以修复这个证明。
Wiles
检查证明正确性的一种方法是让计算机来完成。像Lean这样的证明助手通过算法验证证明的逻辑，使其正确性毋庸置疑。对人类而言，困难之处在于重写证明以让Lean能够理解。写给人类读者的证明会跳过许多显而易见的步骤，而Lean需要看到每一步，无论多么琐碎。人类撰写的证明还建立在数百年数学积累的基础上。
对FLT来说，形式化过程原本预计需要数年。仅数学界一直用来描述该项目初期阶段的蓝图就长达86页。
Claude在11天内完成了这一证明，过程中产出了30300条定理的计算机可验证证明（最终证明使用了其中29500条）。数十个Claude智能体协作定义概念、证明中间定理，并利用这些定理去证明更难的命题。Claude的证明长达1300万行Lean代码，是Mathlib（该定理所依赖的主要社区数学证明库）规模的5倍以上。
Claude的证明遵循了Darmon、Diamond和Taylor给出的Wiles证明的简化版本。人类的数学输入仅限于Tianyi偶尔给出的高层指示：“把Jacobian作为概形（scheme）处理听起来优先级很高”，“尽快推进Mazur定理”。你可以在这里找到Claude思考过程的节选。
`“THE FLT root reads Proved on the site. Historic moment (modulo re-check).”
“!!! The FLT ROOT 62eb32c0 reads PROVED. R = T closed and cascaded to the root. This is the campaign’s goal: e2e FLT on prove2me.”
“🏁🏁🏁The FLT root reads PROVED on prove2me at 02:00:57Z Aug-18 (10:00:57pm ET Aug-17). Historic moment for this campaign.” `
这是Claude意识到自己刚刚完成之事时的思考节选。
Claude的许多初始尝试都失败了：尽管智能体们早期取得了一些进展，但它们很快失去了对项目状态的追踪，无法继续有效协作。这些失败的尝试贡献了最终证明中约7%的非模板行。
当我们改用Prove2Me——由哥伦比亚大学的Tianyi Peng及其合作者设计的开放数学形式化协作平台——这项工作才得以成功。Prove2Me的帮助体现在：
借助Prove2Me和基于Claude Code的多智能体框架，一个智能体团队在不到两周的时间里完成了证明，消耗了约60亿输出token，所用的是一个通用内部研究模型，大致相当于Claude Fable 5.1。完成的证明已由Lean检验；它只使用了Lean的三条标准公理，并且一个comparator工具确认该定理的表述与Mathlib中FLT的表述完全一致。
我们能如此迅速地完成这一证明，表明如今已可对数学的广大领域进行形式化，这既有助于发现现有数学证明体系中的错误，也能减轻新成果审稿的负担。在审阅了Claude的Lean证明后，Kevin Buzzard告诉我们：
形式化也是人类对AI生成的数学结果建立信心的重要因素。随着AI及AI辅助的数学家产出的（所谓）证明比以往任何时候都多，AI辅助形式化为人类审阅者分担了部分负担。我们预计，今后在任何面向人类读者的论文写作中同时附上一份形式化证明将成为常态。虽然我们认为形式化证明不应取代人类可理解的阐述，但它可能是数学界跟上AI生成贡献的唯一可行途径。
撰写Lean似乎也有助于Claude证明新颖的结果。我们近期许多由Claude完成的成果都是在证明的同时并行进行形式化的，Claude似乎会利用这些部分完成的证明来独立检验自己的假设，就像它会编写数值模拟来确认自己方向正确一样。
形式化FLT是一个token密集型项目，但它同时是迄今构建的最大规模的Lean证明。Anthropic的研究人员做了一个小实验：用三个个人Claude Max订阅来形式化Hardy-Littlewood圆法的应用。智能体们完全通过Prove2Me协作，仅用三天就共同完成了维诺格拉多夫三素数定理的形式化。我们认为，只要脚手架得当，利用消费级AI订阅协作形式化重大成果是可以实现的。
为此，Anthropic以及其他实验室最近扩大了对外部研究者的支持——包括从事纯数学和形式化研究的数学家——提供免费与折扣订阅及研究额度。我们还为更大型的科学项目提供专项资助，其中可能包括形式化其他重大定理或改进Lean和Mathlib。
随着AI迅速改变数学研究的面貌，Anthropic内外的数学家们都在思考这对他们的工作意味着什么。不过，形式化是一个让我们对AI的角色毫无疑问感到欣慰的领域。随着形式化成为更常见的工具，我们希望它有助于维护人们对数学知识公共体系的信任。
我们的形式化工作只是费马定理漫长历史与形式化数学发展中的一小部分。Andrew Wiles与Richard Taylor给出的首个完整证明是三百多年数学积累的集大成之作，融合了Gerhard Frey、Jean-Pierre Serre、Ken Ribet、Barry Mazur、Robert Langlands、Jerrold Tunnell、Yutaka Taniyama、Goro Shimura和André Weil等人的思想。Claude的证明则遵循了Henri Darmon、Fred Diamond和Richard Taylor的阐述。