姚班校友主导，Claude攻克费马大定理首个完整形式化证明

Anthropic宣布，其AI模型Claude完成了费马大定理的首个端到端形式化证明，全程耗时11天。该证明包含约1300万行Lean代码及超3万个中间定理，代码量是Lean核心数学库Mathlib的五倍以上。此次工作并非发现新证明，而是将数学家Andrew Wiles于1994年完成的经典证明，翻译为计算机可逐行验证的格式。项目由清华姚班校友、哥伦比亚大学助理教授Tianyi Peng主导，他最初仅测试Claude的推进能力，最终AI在协作平台Prove2Me及多智能体系统支持下完成全部工作，人类仅提供高层提示。过程中消耗约60亿输出Token，早期失败代码仅占成品7%。帝国理工学院教授Kevin Buzzard评价其为“非凡的自动形式化成果”。该突破或使依赖人工的数学文献形式化首次具备大规模提速条件。同期，OpenAI正逐步向付费用户开放GPT-6 Astra模型，强化长链路任务与软件工程能力。