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

📋总体概括

Anthropic宣布Claude完成费马大定理首个端到端、可被计算机完整检查的形式化证明，工程耗时约11天，产出约1300万行Lean代码、3万余个中间定理（最终使用约29500个），规模超过Lean核心数学库Mathlib的5倍。项目由姚班校友主导。Claude并未发现新证明，而是将Wiles 1994年完成的人类证明彻底翻译为无「显然」步骤的机器可验证形式，而这本是数学界预计需数年的工程，标志着AI在大规模数学形式化上的工程能力突破。