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开源。
事件分析
技术层面，此项目的突破点不在证明本身（怀尔斯1995年已给出证明），而在自动形式化能力：多智能体通过DAG任务图分工协作、分离定理陈述与证明文件以加速Lean编译、以自然语言描述支持定理检索复用，从而解决了早期尝试中智能体记忆退化与协作失效的问题。产业影响上，数学验证长期依赖人工评审——怀尔斯证明审稿数月、开普勒猜想审稿四年仍未完全定论——机器可检验证明有望大幅压缩评审周期，并为LLM生成的数学内容提供可信度背书。后续看点包括：Prove2Me等自动形式化工具链的开源生态发展，Lean与Mathlib社区同AI实验室的深度绑定，以及消费级订阅即可完成重大定理形式化所暗示的算力成本下降曲线。
核心观点：AI用11天完成预期数年的形式化工程，机器可验证的数学正成为人类信任AI科研产出的新基石。
原文链接：Hacker News
