Anthropic 宣布 Claude 完成费马大定理的 Lean 4 形式化证明，姚班校友主导

清华姚班校友 Tianyi Peng 主导，Anthropic 的 Claude 仅用 11 天完成费马大定理首个端到端、可由计算机完整检查的形式化证明，产出约 1300 万行 Lean 代码、超 3 万个中间定理，代码规模超 Lean 核心数学库 Mathlib 的 5 倍。此次是将人类可读的证明翻译成计算机可逐行验证的形式化证明，过程中多 Agent 协作曾遇混乱，后借助 Prove2Me 平台理顺，人类仅提供少量高层提示。