Claude 完成费马大定理首个完整形式化证明，姚班校友主导
Claude 借助多智能体协作，首次完成费马大定理的端到端形式化证明，展示 AI 在复杂数学推理上的新能力。
Anthropic 宣布，Claude 已给出费马大定理的完整计算机可验证证明。数学家可读的证明被翻译成 1300 万行 Lean 代码，每一步都能被机器检查。项目由姚班校友、哥伦比亚助理教授田一鸣主导，多智能体协作完成，消耗约 60 亿输出 token，并验证了定理与 Mathlib 中的表述一致。
正文摘录
- title: Led by a Yao Class Alumnus, Claude Achieves First Complete Formal Proof of Fermat's Last Theorem - sourcecompany: QbitAI - bodymarkdown: Just now, Anthropic announced that Claude has completed the first end-to-end, fully computer-verifiable proof of Fermat's Last Theorem . A proof that human mathematicians can read, fully translated into a formal proof that a computer can check line by line, with no "it is obvious here" left anywhere. More than 350 years of mathematical history have been packed by Claude into 13 million lines of Lean. First, let's quickly recap what Fermat's Last Theorem actually is. It states that for any integer n 2, there are no positive integers a, b, c such that: aⁿ+bⁿ=cⁿ . From the 17th century, when Fermat left this proposition, a long line of mathematician…