Anthropic称其Claude AI在11天内基本独立完成了一项任务：生成历史上最长的数学证明，并以此形式化证明了费马大定理。该定理困扰数学家358年，最终以1300万行代码呈现，供计算机逐行核查，无需人类信任背书。相比之下，伦敦帝国理工学院自2024年起由Kevin Buzzard领导的人类主导项目尚未完成。

费马于1637年在书页边缘写下该猜想，声称有一个“真正奇妙的证明”，但页边空白太小无法写下。1995年，英国数学家安德鲁·怀尔斯才给出真正证明，但过程中曾发现漏洞，经近一年修复后才发表129页的最终版本。怀尔斯的证明依赖于费马时代不存在的数学工具，因此数学家普遍怀疑费马当初声称的证明并不成立。

Buzzard于2024年发起将怀尔斯证明形式化为Lean语言的项目，预计需数十位志愿者数学家协作，项目大纲长达86页，资金已锁定至2029年。而Claude仅用11天即完成全部工作。

据Anthropic详细说明，哥伦比亚大学AI形式化工具研究者Peng Tianyi让数十个Claude代理并行工作，几乎无人类干预，仅偶尔提示“优先证明此定理”。初期代理常因重复劳动或迷失方向而失败，此类试错约占最终代码的7%。问题通过引入Prove2Me工具解决：该工具为所有代理提供实时待办清单，避免重复工作，同时组织文件结构以提升Lean检查效率，并保留英文注释以便代理复用成果。

最终，Claude证明了超过3万个引理，消耗数十亿token，运行于类似Claude Fable 5.1的研究模型。1300万行代码相当于160部小说的逻辑论证量，是现有数学库Mathlib的五倍以上。

Buzzard审核后确认该证明“除数学公理外无其他假设”。值得注意的是，这并非AI首次独立发现新数学——Anthropic今年早些时候在密码学研究中也声称实现过此类突破。但费马大定理本身早已由怀尔斯证明，Claude的贡献在于构建了一个机器可验证的“收据”。随着AI生成证明越来越多，人类核查速度已跟不上，形式化验证因而显得尤为重要。

历史上，开普勒猜想计算机辅助证明曾耗时四年，评审委员会仅敢宣称“99%确信”；佩雷尔曼对庞加莱猜想的证明也经历了类似漫长的验证周期。目前，这1300万行完整证明已开源发布于GitHub，供任何数学家自行核查。