0
11天、60亿Token、1300万行Lean：Claude形式化费马大定理，AI正在进入“可验证科研”阶段
2026年9月4日，Anthropic公布了一项很容易被“AI又攻克一道数学名题”这种标题掩盖掉技术含量的工作：一个由Claude驱动的多智能体系统，在11天内完成了费马大定理（Fermat’s Last Theorem，FLT）的端到端Lean形式化。官方披露，整个项目生成约1300万行Lean代码，完成30300个可机器验证的定理，最终证明使用了约29500个中间定理，消耗约60亿个输出Token。