Anthropic公司表示，其Claude AI刚刚编写了有史以来最长的数学证明，并借此形式化证明了费马最后定理——这个困扰数学家长达358年的难题。Claude在11天内基本自主完成了这项工作，生成了1300万行代码，计算机可以逐行检查，而不只是听信数学家的断言。
Myriad：GPT-6何时公开可用？点击进行预测。
费马最后定理指出，不能取三个正整数，将每个数提高到大于2的幂次，并使前两个之和等于第三个。1637年，费马将这个断言草草写在一本数学书的页边，并补充说有一个“真正绝妙的证明”，但页边太窄写不下。随后他离世。此后的358年里，数学家们试图重建他当时的想法。
证明与核查是两回事。数学证明是一串逻辑步骤，若一环断裂，整体崩塌。在数百页严密论证中找出那个断裂的环节，可能耗费其他数学家数年的生命。形式化证明意味着将证明翻译成极其字面的语言，让计算机无需主观判断即可自主验证每一步。数学家在这方面一直做得不好。1908年一个相当于如今约100万至200万美元的德国奖项，悬赏第一个有效证明，仅第一年就收到了621份错误投稿。
真正的证明直到1995年才由英国数学家Andrew Wiles给出，且带有转折。Wiles在1993年6月的三场讲座中宣布解法，但后来审稿人发现其中有一个漏洞。他与昔日学生Richard Taylor花费近一年修补，几近放弃，终于在1995年5月发表了修正后的129页证明。该证明依赖费马时代不存在的数学，这也是数学家现在怀疑费马本人“绝妙证明”可能从未成立的重要原因。
伦敦帝国理工学院数学家Kevin Buzzard在2024年启动了一个项目，要做正是Claude刚做的事：将Wiles的证明翻译成计算机可检查的Lean语言。这类工作通常需要大批志愿数学家——项目大纲就有86页，资金已锁定至2029年。而Claude只用了11天就完成了全部。
Claude如何做到？Anthropic在一篇深入博文中解释，哥伦比亚大学构建AI形式化工具的Tianyi Peng决定测试Claude能自主走多远。数十个Claude智能体并行工作，编写定义、证明小结论，并堆叠成更大成果，几乎无人工介入，仅有偶尔如“优先证下一个定理”的推动。起初并不顺利：智能体常丢失已证内容、停止协作，这些失败尝试仍占最终证明的约7%行数。解决方法是Peng团队构建的Prove2Me工具，它为每个智能体提供相同的实时待办列表，避免重复或偏离。它还组织文件以加快Lean检查，并保留每条结果的英文笔记，便于智能体复用。
Anthropic称，人类可能在拖慢进程——AI已在开发AI。完成时，Claude证明了逾3万个辅助定理，消耗数十亿token，运行在类似于后来公开发布的Claude Fable 5.1的研究模型上。成品证明长达1300万行，是数学家常用共享库Mathlib的5倍多。典型小说约8万字，Claude的证明相当于160部纯逻辑论证的小说。
这真的有意义吗？Buzzard（其自家项目资金仍到2029）审阅了Claude的证明并祝福，称其“除数学公理外无假设”地证明了该定理。这不同于Claude今年早些时候在密码学研究中声称的发现全新数学。Wiles三十年前已证，Claude只是建了机器可查的收据。其价值在于数学家正被未验证证明（包括AI写的）淹没，快过人手核查速度。且此类证明确定性强、无人类错误，至关重要。这非新问题：计算机辅助的Kepler猜想证明花了四年才获评审“99%确定”；Perelman的庞加莱猜想证明也花了约同样长时间被消化。若不愿轻信Anthropic，完整1300万行证明已置于GitHub，任何有空闲的数学家皆可逐行挑剔。