AI 助力数学突破：Claude 11 天完成费马大定理形式化验证

英国数学家安德鲁・怀尔斯 1995 年完成的费马大定理证明，近日由 Anthropic 公司的 AI 模型 Claude 自主运行 11 天后完成形式化验证，生成超 1300 万行代码并验证 3 万余个定理。该项目采用多智能体协作及有向无环图技术管理定理依赖，人类仅提供高层次指导，全程消耗约 60 亿输出 Token，使用 Claude Fable 5.1 级别的内部模型。Lean 证明助手凭借严格验证机制参与其中，且仅用 3 条标准公理确保证明纯粹性。数学形式化专家认为这是 AI 辅助数学研究的重大突破，过去需数学家数年完成的复杂证明形式化工作被 AI 大幅加速。完整证明代码已在 GitHub 公开，Anthropic 表示未来为传统证明同步提供形式化版本或成行业标准，可降低新理论验证的人工成本。