Claude 11 天形式化费马大定理：1300 万行 Lean 代码创纪录

AI寒武纪 · wechat · 2026-09-05

Anthropic 研究员 Tianyi Peng（清华姚班、MIT 博士、哥大助理教授）团队让 Claude 在 11 天内近乎全自主完成了费马大定理的完整 Lean 机器验证，总代码量超 1300 万行（约为 Mathlib 的 5 倍），尝试证明 30300 个定理、采纳 29500 个衍生定理，消耗约 60 亿输出 Token，博客与代码均已公开。

关键在于哥大研发的 Prove2Me 协同平台：定理有向无环图解决智能体上下文遗忘与并行协作，陈述与证明分离提升编译效率，自然语言描述便于检索复用。人类干预极少，仅偶发宏观提示。Kevin Buzzard 评价该自动形式化成果除数学公理外无额外假设，标志着现代数学文献全面机器验证迈出大步。团队还用 3 个普通 Claude Max 订阅 3 天完成维诺格拉多夫三素数定理形式化，证明消费级订阅即可操作。