Claude 用 11 天攻克费马大定理：1340 万行 Lean，没有一句“显然”

9 月 4 日，Anthropic 展示了费马大定理的首次完整机器测试。 Claude 在 11 天的时间里，几乎没有人的帮助，将 Andrew Wiles 的证明翻译成Lean 语言：1340 万行代码，大约 3 万个中间定理，“从所说的内容中显而易见”为零。这个项目是数学家们筹划多年的——只有伦敦帝国理工学院的凯文·巴扎德 (Kevin Buzzard) 绘制的第一阶段图就长达 86 页——在一周半的时间里就完成了。

让我们立即澄清一下这里没有的内容：没有新的证据。该模型没有提出自己的定理路径。她做了一些不同的事情，坦率地说，也同样复杂——她进行了人工证明，每一页上都有诸如“这很简单”之类的免责声明，并重写了它，以便编译器检查每个步骤。 1995年以后的数学家对该定理的信心为99.9%。现在你可以百分百了：Lean已经贯穿了三个标准公理的整个推导过程，没有什么可怀疑的了。

电脑到底检查了什么？

数字在这里比绰号更合适。

• Lean 的 1340 万行比整个 Mathlib（系统主要的形式数学库）大五倍多。
• 已证明约3万个中间定理；最终产量约为 29,500 份。
• 在 96 核机器上编译存储库大约比编译 Mathlib 花费的时间长 20 倍。在测试期间，Buzzard 获得了一台具有 500 GB RAM 的服务器。
• 仅依赖三个标准公理 Lean。没有“简单的假设”。

Kevin Buzzard 是自 2024 年以来一直领导社区 Fermat 形式化项目的数学家，他下载了存储库，组装了它并运行了比较器：定理的输出公式与 Mathlib 的参考公式一致，所有检查都是绿色的。他的评论是：“自动形式化的非凡成就。”

页边空白处的一行，三个半世纪的工作

1637 年左右，皮埃尔·德·费马 (Pierre de Fermat) 将丢番图算术页边的陈述归因于：对于 n 大于 2 的情况，方程 aⁿ + bⁿ = cⁿ 在自然数中没有解。下面是一句已成为传奇的短语：“我找到了一个真正精彩的证明，但边缘太窄了。”从欧拉到库默，一代又一代的数学家都在逐步走向这个结果。 1908年，颁发了10万金马克的证明奖，第一年就收到了621个错误的答案。

1993 年 6 月，安德鲁·怀尔斯 (Andrew Wiles) 在剑桥的一系列讲座中提出了他的证明。两个月后，一位审稿人提出了一个问题，揭示了其中一个设计中的一个漏洞。怀尔斯花了一年的时间修补了它——先是独自一人，然后与以前的学生理查德·泰勒一起——几乎要放弃一切，并于 1995 年出版了一篇 129 页的文本。最后一个“工程”问题仍然存在：是否有可能迫使计算机完整地确认这一切？

不是新的证据，而是新的机会

它基于 Darmon、Diamond 和 Taylor 1995 年通过 Langlands-Tunnell 定理和 Ribet 水平下降对 Wiles-Taylor 论证的分析。荷兰计算机科学家 Jan Bergstra 在 2000 年代就提出了将怀尔斯形式化的想法，但直到最近，这还被认为是整个科学方向的工作。个别病例 - 四级、常规简单病例 - 已提前移至 Lean。有了新的存储库，Weidik 的 100 项形式化任务的整个列表就结束了：与该领域进行比较的基准已有 20 年历史。

顺便说一句，巴扎德诚实地写道：从数学上来说，这项工作并没有揭示任何新东西——他已经相信怀尔斯了。价值在别处。审阅一篇新的数学文章需要几个月甚至几年的时间；如果可以要求机器即时形式化证明，同行评审将会缩小，专家级别的隐藏假设将开始浮出水面。对于一切都依赖于结论的诚实性的科学来说，这是一个严重的转变。

从内部看那11天是什么样的

这项工作由 Anthropic 研究员 Tianyi Peng 领导，他之前在哥伦比亚大学组装了一组人工智能形式化工具。据他透露，他最初并没有打算走到最后：他只是想看看Claude能将Buzzard的项目推进多少。晋级决赛。

许多智能体并行工作：一些完成了数学定义，其他人猛攻中间引理，其他人沿着定理树向上移动，还有一些人将各个部分重新组装成一个结论。第一天就出了问题——代理们失去了项目的整体情况，大约百分之七的早期尝试仍然保留在最终代码中。当团队转移到 Prove2Me 平台时，情况发生了转变：其中的证明是定理节点图，您可以在其中看到已经证明的内容、等待先决条件的内容以及下一步要采取的内容。陈述与证明分离，编译加速，每个定理都有可搜索的文本描述。工作规模约为六十亿产出代币，人工提示被简化为高级：“这个方向是优先级”。

在哪里观看

该存储库发布在 GitHub 上 - 如果您愿意，如果您有一台具有 96 核和强大神经的机器，您可以自己运行检查。主要来源： 来自人择的分析 和 秃鹰的帖子 在 Xena 项目博客上。

如果在看完 1300 万行的故事后，您想了解现代模型如何处理较小的任务（算法、代码、计算），请查看以下部分 “代码” 和 “聊天” 在 NeuralSpace 上：您可以在那里试验模型并通过 API 将它们连接到您的项目。