11天！Claude完成费马大定理千万行机器验证

近期一项人工智能领域的突破引发了全球数学界的震动：AI模型Claude仅用11天时间，就近乎完全自主地完成了费马大定理的完整机器验证代码编写。这也是迄今为止规模最大的Lean形式化证明项目，总代码量超过1300万行，几乎是当前主流数学形式化公共库Mathlib规模的五倍。为了完成这一目标，Claude在推导过程中额外证明了29500个衍生数学定理，覆盖了代数、调和分析、几何与数论等多个此前从未被形式化过的数学分支。

目前相关官方研究博客与完整开源代码已经对外公布：

官方研究博客链接：https://anthropic.com/research/formalizing-fermats-last-theorem

GitHub开源地址：https://github.com/anthropics/fermats-last-theorem

跨越三个半世纪的数学难题

1637年左右，法国数学家皮埃尔·德·费马在阅读《算术》一书时，在书页空白处写下了一个著名断言：当整数n大于2时，不存在正整数a、b、c满足aⁿ + bⁿ = cⁿ。他还留下了一句广为流传的批注：“我发现了一个真正奇妙的证明，可惜这里的空白太小，写不下。”

为了验证这个猜想，全球数学家耗费了超过350年的时间。1908年，德国学术机构设立了10万马克的奖金悬赏正确证明，仅发布第一年就收到了621份错误的解答方案。直到1995年，安德鲁·怀尔斯才正式攻克了这一难题。

怀尔斯在1993年6月通过三场系列演讲公布了长达129页的证明草稿，但经过两个月的同行评审后，审稿人指出了证明中存在致命漏洞。随后他闭关研究一年，先是独自尝试修复，之后与学生理查德·泰勒合作，在即将放弃之际找到了修正方法，并于1995年5月正式发表了完整论文。

现代数学界普遍认为，费马当年口中的“奇妙证明”大概率是错误的，因为怀尔斯的证明用到了17世纪尚未出现的现代数学工具。这套最终的证明融合了弗雷、塞尔、里贝特、梅祖尔、朗兰兹等数十位数学家的开创性研究成果，凝结了几代数学人的智慧。

为何需要机器进行形式化验证

传统的数学论文是写给人类阅读的，作者往往会跳过大量被认为“显而易见”的推理步骤，并且默认基于数个世纪以来的海量学术文献基础。但计算机无法理解“显然成立”这类模糊表述，像Lean这类交互式定理证明工具，要求将所有推理拆解为机器可以直接读取的逻辑形式，从最基础的数学公理出发，一步步完成完整推演。只要最终代码能够通过Lean的编译，就意味着整个证明在逻辑上不存在任何纰漏，百分之百严谨可靠。

2005年，荷兰计算机科学家Jan Bergstra首次提出对怀尔斯的费马大定理证明进行形式化验证的设想。2024年，帝国理工学院的数学家凯文·巴扎德在社区发起了这项浩大的工程，仅初始阶段的项目规划蓝图就长达86页，当时学界普遍认为这需要全球数学家合力耗费数年时间才能完成。

Anthropic的研究员Tianyi Peng决定测试人工智能能否加速这一进程。主持这项研究的Tianyi Peng有着扎实的学术背景：他早年是信息学竞赛的顶尖选手，曾获得全国青少年信息学奥赛选拔赛第八名，2017年本科毕业于清华姚班，2023年获得麻省理工学院博士学位，目前担任哥伦比亚大学助理教授，同时也是Anthropic的研究员，长期带领团队开展强化学习、AI智能体以及形式化工具的研发工作。

Tianyi Peng曾亲身经历过缺乏形式化验证的困扰：当年他的导师希望将他的论文成果推荐给顶刊，但询问他能否确保证明完全没有差错时，他只能回答只有99%的把握，对于长达数十页的证明来说，很难做到100%的严谨确认，最终这项成果错失了登上顶级学术期刊的机会。

人类审查超长且复杂的数学证明本身就极为吃力。1998年托马斯·海尔斯证明开普勒猜想时，12位审稿人花费了4年时间审核，最终只能得出“99%可能正确”的结论，海尔斯后来不得不组建二十多人的团队，通过Flyspeck项目耗时多年完成形式化验证。佩雷尔曼解决庞加莱猜想后，数学界花费了4年时间撰写三部数百页的详尽解析，才最终确认证明的正确性。2013年哈拉尔德·赫尔夫戈特提出的弱哥德巴赫猜想证明，至今仍处于同行评审阶段。数学界甚至曾出现过接受错误研究成果长达数年的情况，导致后续学者在有缺陷的基础上开展研究。而机器形式化验证，正是解决这类学术信任危机的终极方案。

11天与60亿Token的攻坚历程

Tianyi Peng团队为Claude设定的证明路线，参考了达蒙、戴蒙德与泰勒对怀尔斯证明的精简阐述版本，使用的模型能力大致相当于Claude Fable 5.1的通用内部研究模型。项目初期的尝试并不顺利：多个AI智能体虽然在早期取得了一定进展，但很快会丢失整个项目的全局状态，无法实现有效协同，最终生成的代码中约7%的行数属于无效的失败尝试。

直到团队引入了哥伦比亚大学研发的Prove2Me协同平台后，局面迎来转机。Prove2Me平台主要实现了三项核心功能：第一，构建定理的有向无环图，让AI智能体能够清晰掌握整体项目进展与依赖关系，自主决定下一步需要攻克的子定理，解决了传统模式下的上下文遗忘问题，同时支持多个智能体并行开展工作；第二，将定理的陈述与具体证明过程拆分到不同文件中，独立维护两者之间的链接关系，大幅降低了计算资源消耗，提升了Lean的编译效率；第三，为每个定理维护自然语言层面的描述，帮助智能体在庞大的知识库中快速检索和复用已有结论，从而找到更简洁的证明路径。

随后数十个Claude智能体开始分工协作，从定义基础数学概念开始，逐步证明中间定理，再利用这些中间成果攻克更复杂的命题。人类的干预极少，仅由Tianyi Peng偶尔给出宏观方向提示，比如调整雅可比定理的优先级，或是催促推进梅祖尔定理的证明。Claude的完整思考日志PDF也已对外公开。

在证明闭环完成的那一刻，Prove2Me平台上的费马大定理根节点被标记为已证明，这是历史性的一刻。协调世界时8月18日凌晨2点，费马大定理的形式化验证被正式确认完成。最终，Claude总共尝试证明了30300个定理，其中29500个被纳入最终的证明体系，整个过程消耗了约60亿输出Token。这份形式化证明仅依赖Lean的三条标准公理，经过比对工具确认，其最终陈述与Mathlib库中对费马大定理的标准定义完全一致。

对未来数学研究的深远意义

与近期AI在黎曼猜想研究中尝试提出全新数学思路不同，这次Claude的突破核心在于全流程的自动形式化验证。看过这份Lean代码后，凯文·巴扎德评价道：“这项非凡的自动形式化成果仅用11天就完成，除了基础数学公理外没有任何额外假设。我们看到代数、调和分析、几何与数论都被自动化形式化，这证明AI生成的中间产物已经足够稳固，可以逐层向上构建复杂的数学体系。如果费马大定理的自动形式化在今天已经可行，那么全面实现现代数学文献的机器验证就迈出了关键的一大步。”

AI编写Lean代码不仅可以用于验证现有证明，还能反哺新的数学成果发现。研究团队注意到，Claude在许多新的探索中会一边推导数学结论，一边编写形式化证明代码，就像通过数值模拟验证研究思路一样，借助这些部分完成的证明来独立确认自己的猜想是否走在正确的轨道上。

形式化验证重大数学定理并非算力巨头的专属特权。研究团队使用3个普通的Claude Max个人订阅账号开展了实验，同样依托Prove2Me平台，让智能体协作使用哈代-李特尔伍德圆法，仅用3天就完成了维诺格拉多夫三素数定理的形式化验证。这意味着普通研究人员使用消费级订阅服务完成重大数学命题的形式化验证，已经具备了实际操作的可行性。

为了推动这一趋势，Anthropic正在联合其他实验室扩大对外部数学家的支持，包括提供免费或折扣的订阅服务、科研算力额度，以及为形式化其他重大定理、改进Lean与Mathlib库的研究项目提供专项资助。人类数学家此前耗费数年甚至数十年进行论文审查的沉重负担，正在被人工智能技术彻底卸下。

参考资料

Tianyi Peng团队关于协作平台的最新论文：《Prove2Me: An open collaborative platform for scaling math formalization》，arXiv链接：https://doi.org/10.48550/arXiv.2608.28433

GitHub仓库中包含完整的代码实现以及证明步骤的详细文字解读。