Claude耗时11天完成费马大定理完整形式化证明

9月4日，Anthropic正式宣布，由清华姚班校友彭天翼发起的项目成功在11天内完成费马大定理的首个完整形式化证明。该成果依托自主研发的数学协作平台Prove2Me，调度数十个Claude智能体并行计算，最终生成约1300万行Lean代码，验证逾2.95万个中间定理，消耗约60亿输出Token。 面对传统数学审查耗时极长的行业痛点，系统沿袭怀尔斯经典证明路径，将反证法、Frey曲线构造与模性提升等复杂逻辑转化为可逐层核验的代码。Prove2Me平台通过分离定理陈述与证明、维护依赖图谱及支持分步草图提交，有效攻克了多智能体协作中的状态同步难题。项目最终仅依赖Lean基础公理，并引入独立Rust内核交叉核验，彻底排除逻辑缺口与命题篡改风险。 尽管部分代码仍需人工精简以适配人类阅读与复用标准，但此次实践证实了大模型处理超大规模数学形式化工程的算力与逻辑调度实力。它不仅为数学成果提供了可机器复核的全新范式，也为未来AI生成内容的质量审查机制确立了坚实的技术基准。