Anthropic 表示，Claude 已完成费马大定理的首个完整形式化证明。这不是重新发现这一定理，而是把既有证明转写为计算机可逐行核验的逻辑代码。公司称，这项工作用时 11 天，最终生成约 1300 万行内容。
形式化证明的意义，在于把数学论证写成机器可检查的语言。传统论文证明往往需要同行长期复核，一旦中间某一步有漏洞，修补过程可能持续数月甚至数年。费马大定理由英国数学家 Andrew Wiles 于 1995 年完成证明，但要把这套证明完整转成可机检版本，一直被视为高强度工程。
11天完成长期项目目标
伦敦帝国理工学院数学家 Kevin Buzzard 从 2024 年起推动相关项目，目标同样是把 Wiles 的证明转写到 Lean 证明助手中。按原计划，这项工作需要长期协作，资金已安排到 2029 年。
Anthropic 称，Claude 在这一任务上提前完成了同类目标。Buzzard 审阅后表示，这份证明能够在不依赖额外假设的情况下成立，也就是只基于数学最基本的公理系统完成验证。
由多代理并行完成
据 Anthropic 介绍，哥伦比亚大学研究人员 Tianyi Peng 团队让多个 Claude 代理并行工作，分别负责编写定义、证明较小结论，再逐步拼接成更大的证明结构。人工干预较少，主要是给出阶段性优先顺序。
早期进展并不顺利。Anthropic 称，部分代理一度无法共享已完成内容，也会重复工作。随后，团队使用名为 Prove2Me 的工具，为各代理提供统一任务清单和文件组织方式，并保留自然语言备注，帮助它们复用彼此结果。
- 支撑性定理超过 3 万个
- 总消耗达到数十亿 token
- 最终证明约 1300 万行
重点在可验证而非新定理
这次成果的重点，不在于发现全新的数学命题，而在于把已有重大证明变成可由计算机逐步核验的版本。随着数学论文和 AI 生成内容增加，人工逐条检查证明的成本也在上升，形式化工具因此更受关注。
Anthropic 还称，这份证明规模已超过数学界常用共享库 Mathlib 的 5 倍以上。完整文件已上传至 GitHub，研究人员可以继续逐行审查其结构与正确性。
