共计 1211 个字符，预计需要花费 4 分钟才能阅读完成。
姚班校友主导,Claude 攻克费马大定理首个完整形式化证明
最后靠 Harness 救回来
导语: 费马大定理早已由人类数学家证明, 但让计算机逐步核验整套证明 , 仍是极高难度的工程。Anthropic 最新披露的一项实验显示,Claude 在多 Agent 协作框架下, 完成了一个可由 Lean 检查的端到端形式化版本。
📌 从“人能读懂”到“机器能检查”
费马大定理的表述并不复杂: 当整数 n>2 时, 不存在正整数 a、b、c 使得 an+bn=cn。这个命题由费马提出后, 经历了数百年推进, 直到 Andrew Wiles 与 Richard Taylor 在上世纪 90 年代完成被数学界接受的证明。
此次 Claude 并不是发现了新的数学证明路线 , 而是把已有的人类数学证明转写为 Lean 能够逐行验证的形式化证明。对于证明助手而言, 论文中常见的“显然”“容易得到”等跳步都必须被拆成明确的定义、引理和推导。
🔍 约 1300 万行 Lean 代码, 规模超过 Mathlib
团队还表示, 最终证明依赖 Lean 的三个标准公理, 并通过程序对比确认,Claude 形式化的费马大定理陈述与 Mathlib 中对应陈述一致。换言之, 判断证明是否成立的并不是模型自我声明, 而是 Lean 的形式化检查结果。
💡 多 Agent 协作并非一开始顺利
项目早期曾尝试让多个 Agent 并行推进: 有的补充定义, 有的处理引理, 有的向更高层定理推进。但随着工程规模扩大,Agent 对整体进度和依赖关系的把握变得困难, 早期尝试留下的代码最终只占成品非模板代码的一小部分。
转折点来自 Prove2Me 平台, 以及基于 Claude Code 的 multi-agent harness。该系统将证明拆解为由定理节点组成的有向无环图, 让 Agent 能够理解哪些节点已完成、哪些仍缺前置条件, 并围绕任务依赖进行分工。
- 任务拆分: 把庞大证明拆成可追踪的定理节点。
- 协作管理: 分离定理陈述与证明过程, 便于复用和检索。
- 编译优化: 加速 Lean 检查, 降低大型工程反复验证成本。
- 人类介入: 研究人员主要提供高层方向提示, 而非逐条编写证明。
📊 数学形式化可能迎来提速窗口
这项实验由 Anthropic 研究员 Tianyi Peng 主导。他曾就读清华姚班, 后获 MIT 博士学位, 目前同时任哥伦比亚大学助理教授与 Anthropic 研究员。负责审阅结果的 Kevin Buzzard 将其称为一次“非凡的自动形式化成果”。
值得注意的是, 数学形式化长期被认为是一类高门槛、重工程、进展缓慢的工作 。若 AI 能在复杂依赖管理、引理生成和证明拼装中承担更多任务, 未来对经典数学文献进行大规模形式化, 或许会比过去更可行。
🚀 总结:AI 的价值在“严密搬运”
从目前已知信息看,Claude 的突破更适合理解为一次大型数学工程自动化实验, 而不是数学创造力的终局答案。它展示了大模型、形式化工具和多 Agent 项目管理结合后的潜力: 让机器把人类证明搬进可验证系统, 并接受严格检查。
