Anthropic 旗下 AI 模型 Claude 在数学形式化领域取得里程碑式突破：仅用 11 天，近乎全自主地完成了费马大定理（Fermat's Last Theorem）的完整机器验证代码编写。
这是迄今为止规模最大的一套 Lean 形式化证明，总代码量超 1300 万行，相当于现有数学公共库 Mathlib 规模的 5 倍。在此过程中，Claude 推导并证明了 29500 个衍生定理，覆盖代数、调和分析、几何及数论等多个此前未被形式化的数学领域。
目前，官方博客与完整代码已开源：
博客链接：https://anthropic.com/research/formalizing-fermats-last-theorem
GitHub 地址：https://github.com/anthropics/fermats-last-theorem
困扰人类 350 年的数学空白
1637 年，法国数学家皮埃尔·德·费马在阅读《算术》时提出断言：当 n>2 时，方程 aⁿ + bⁿ = cⁿ不存在正整数解。他 famously 写道：“我发现了一个真正奇妙的证明，可惜页边空白太小，写不下。”
为填补这一空白，人类数学家探索了 350 余年。1908 年德国设立的巨额悬赏曾引来数百个错误解答。直到 1995 年，安德鲁·怀尔斯（Andrew Wiles）才彻底攻克此难题。
怀尔斯的证明过程极具波折：1993 年他首次公布长达 129 页的证明草稿，但在同行评审中被发现存在致命漏洞。历经一年闭关苦修，并在学生理查德·泰勒协助下修复缺陷后，该证明于 1995 年正式发表。
现代数学界普遍认为，费马当年的“奇妙证明”大概率有误，因为怀尔斯的证明依赖了 17 世纪尚不存在的现代数学工具。这套证明凝聚了弗雷、塞尔、朗兰兹、谷山丰、志村五郎等众多数学家的开创性成果。
为何需要机器进行终审验证
传统数学论文面向人类读者，常省略显而易见步骤或依赖海量文献背景。然而计算机不具备这种“直觉”，Lean 等交互式定理证明工具要求将所有推理拆解为基于基础公理的严密逻辑链，任何一环出错都将导致整体失效。
一旦 Lean 编译通过，即代表该证明在逻辑上百分之百成立，无任何纰漏。
早在 2005 年，Jan Bergstra 便提议对怀尔斯的证明进行形式化。2024 年，帝国理工学院数学家凯文·巴扎德（Kevin Buzzard）发起该项浩大工程，原定计划需全球数学家协作数年。
Anthropic 研究员彭天一（Tianyi Peng）决定测试 AI 能否加速这一进程。彭天一背景深厚：清华姚班本科毕业，MIT 博士，现任哥伦比亚大学助理教授及 Anthropic 研究员，主攻强化学习与形式化工具研发。
彭天一曾因缺乏形式化验证而错失论文登上《Nature》的机会，这让他深刻认识到机器验证的重要性。历史上，海尔斯证明开普勒猜想耗时 4 年审核仍仅获 99% 确信度；佩雷尔曼的庞加莱猜想证明亦耗费学界 4 年解析确认。机器形式化验证正是解决此类信任危机的终极手段。
11 天与 60 亿 Token 的攻坚历程
研究团队基于达蒙、戴蒙德和泰勒对怀尔斯证明的精简版设定路线，使用能力约等于 Claude Fable 5.1 的内部模型进行攻关。
初期尝试并不顺利，智能体易丢失全局状态，导致约 7% 的代码为无效劳动。转折点在于引入了哥伦比亚大学研发的 Prove2Me 协同平台。
Prove2Me 平台通过三大机制提升效率：
构建依赖图谱
建立定理的有向无环图，使智能体能清晰掌握整体进展与依赖关系，支持多智能体并行工作，有效解决上下文遗忘问题。
分离陈述与证明
将定理陈述与具体证明过程分文件维护，降低计算资源消耗，显著提升 Lean 编译效率。
自然语言索引
为每个定理维护自然语言描述，便于智能体在庞大知识库中快速检索复用，寻找更短证明路径。
在数十个 Claude 智能体的分工协作下，人类干预极少，仅由彭天一提供宏观方向提示。UTC 时间 8 月 18 日凌晨 2 点，费马大定理根节点状态被标记为“已解决”。
最终，Claude 共尝试证明 30300 个定理，其中 29500 个被采纳，消耗约 60 亿输出 Token。整个证明仅依赖 Lean 三条标准公理，且经比对确认与 Mathlib 库定义完全一致。
对未来数学研究的深远意义
此次突破的核心在于全流程自动验证。凯文·巴扎德评价道：“这项成果仅用 11 天且无额外假设，证明了 AI 生成的中间产物足够稳固，可层层向上构建。若费马大定理可自动形式化，现代数学文献的全面机器验证将迈出一大步。”
AI 不仅能核验旧知，还能反哺新知发现。研究人员观察到，Claude 在推导过程中会利用部分证明独立核验猜想，类似数值模拟的作用。
此外，形式化大定理不再是算力巨头特权。实验显示，普通研究人员使用消费级订阅账号配合 Prove2Me 平台，仅用 3 天便完成了维诺格拉多夫三素数定理的形式化验证。
为推动这一趋势，Anthropic 正联合其他实验室扩大对外部数学家的支持，提供免费折扣订阅、科研算力额度及专项资助，致力于卸下人类数学家沉重的审查负担。
参考资料
彭天一团队关于协作平台的最新论文：Prove2Me: An open collaborative platform for scaling math formalization
arXiv 链接：https://doi.org/10.48550/arXiv.2608.28433
GitHub 仓库包含完整代码实现及详细文字解读。