Anthropic AI耗时11天、耗资30万美元完成费马大定理形式化证明

事件概述

Anthropic近日宣布，其AI模型Claude在基本自主运行11天后，成功完成了费马大定理（Fermat's Last Theorem）的首个端到端、可由计算机完整检查的形式化证明。这一成果被视为数学界与人工智能结合的重要里程碑，证明了AI有能力将人类复杂的数学直觉转化为机器可逐行验证的逻辑链条。

核心信息与技术细节

• 背景与挑战：费马大定理由皮埃尔·德·费马于1637年提出，安德鲁·怀尔斯于1995年完成人类可读的证明。然而，传统数学证明依赖“显而易见”的直觉省略，计算机无法直接理解。将其转化为机器可读形式需使用Lean等严格的形式化验证工具，此前预计需数年时间的人工投入。
• 执行过程：
  • 多智能体协作：Anthropic调用数十个Claude智能体并行工作，分别负责补全定义、推导引理及整合定理。
  • 解决协作难题：初期智能体因上下文遗忘导致协作停滞。项目发起者、Anthropic研究员彭天翼（Tianyi Peng）团队开发了Prove2Me工具，通过将有向无环图（DAG）记录定理依赖关系，解决了全局进度追踪和任务分配问题。
  • 人类干预极少：人类仅提供高层方向指导（如优先完成Mazur定理），具体推导由AI自主完成。
• 产出规模：最终生成的Lean代码长达1300万行。若按每页50行打印，相当于520本500页的学术专著。

成本与效率对比

• 计算成本：使用性能相当于Claude Fable 5.1的内部研究模型，消耗约60亿输出Token，总成本约为30万美元。
• 横向对比：相比之下，OpenAI此前发布十项数学难题突破性成果并附带机器验证证书，总成本仅约2,000美元。这反映出当前AI在“验证已有结论”上的成本仍高于“探索新发现”，但也体现了形式化证明的高昂门槛。

学界反应与影响

• 高度评价：伦敦帝国理工学院教授Kevin Buzzard（该项目开源计划发起人）评价其为“非凡的自动形式化成就”，指出证明过程除公理外不依赖额外假设。多伦多大学数论学家Daniel Litt表示：“如果他们能形式化费马大定理，那他们大概能形式化任何东西。”
• 审慎观点：菲尔兹奖得主陶哲轩指出，AI在解题和验证正确性上具有优势，但在清晰表述和被学术共同体接受方面进展缓慢。他警告存在**“证明消化不良”**的风险，即AI生成速度远超人类理解与教学转化能力，导致知识难以被有效复用。
• 结构性变化：1300万行代码无人能从头通读，意味着数学知识的“可验证性”与“可理解性”正在分离。虽然AI未提供新的数学定理，但它证明了将复杂数学成果转化为机器独立验证形式的可行性。

关键结论

费马大定理的形式化并非终点，而是现代数学全面机器验证的起点。随着AI能以超越人类的速度生成可验证知识，数学界面临的核心问题已从“能否做到”转向“如何适应这种新型知识生产与验证范式”。