Claude 11天自主证明费马大定理：1300万行Lean代码创史上最大形式化证明

Anthropic宣布，其AI模型Claude在11天内基本自主完成了费马大定理的首个端到端机器验证证明，全部以Lean编程语言写成，代码量达1300万行，验证了30300条定理（最终证明使用其中29500条），规模超过数学社区主库Mathlib的5倍。该证明遵循Darmon、Diamond和Taylor对怀尔斯证明的简化版本，人类参与仅限于少量高层指导。项目由哥伦比亚大学研究员彭天翼发起，采用基于Claude Code的多智能体架构和开源协作平台Prove2Me，通过维护定理有向无环图（DAG）协调数十个Claude智能体并行工作，共消耗约60亿输出token。伦敦帝国理工学院的Kevin Buzzard审阅后确认，该证明除数学公理外不依赖任何额外假设，且与Mathlib中费马大定理的表述一致，而此前数学界预计这项形式化工作需耗时数年。研究团队另以三个Claude Max订阅账号在3天内完成了维诺格拉朵夫三素数定理的形式化。Anthropic认为，自动化形式化技术将帮助检测现有数学文献中的错误、减轻同行评审负担，并为验证AI生成的数学结果提供可靠途径。完整证明已在GitHub开源。

事件分析

核心观点：AI用11天完成预期数年的形式化工程，机器可验证的数学正成为人类信任AI科研产出的新基石。