01
AI 用 11 天把费马大定理的证明翻译成了机器能逐行核验的代码。它 没有证明任何新东西 ，却把一个老问题重新摆上了台面。
9月4日，Anthropic发了一条公告。
Claude，用11天，完成了费马大定理的首个完整 形式化 证明。
数字堆在后面，一个比一个吓人。约1300万行Lean代码，相当于数学公共库Mathlib体量的5倍以上。3万多个定理，其中2.95万个中间定理被纳入最终证明。全程只用Lean的3条标准公理，没有一个未证明的占位符。
这项工作由Anthropic研究员彭天翼发起。他是清华姚班校友，此前和哥伦比亚大学的合作者一起开发过数学形式化协作平台。几十个Claude智能体在这个平台上协作，把这件事啃了下来。
数学界原本预计，人类完成它需要10年。
消息传开，惊叹和质疑一样多。而质疑里，藏着那个更大的问题。AI都这水平了，数学家还有什么用？
CHAPTER 01 · CLARIFICATION
先纠正一个误会
Claude没有证明费马大定理。
0
评论 (0)