Claude 11 天完成费马大定理的机器证明

我在高中微积分课上看过 1996 年关于费马大定理（FLT）的纪录片。对我来说，这永远地确立了我心目中“聪明人”图腾柱顶端的那种现代数学研究者的形象。

这也让我确信自己对该领域毫无兴趣。撇开那种为了得出一个证明而必须进行的苦行僧式工作不谈——这种证明只能通过在该问题空间中抽象且极度小众的孤立环境中苦熬数年才能触及（更别提你可能永远找不到它，或者它根本不存在）——那种痛苦在于，最终的产出是一篇论文、一场演讲或其他人类符号的产物（本质上就是_文字_），而这些东西随时可能因为某个人发现的一个错误而被推翻——这对我来说听起来就像地狱。

如今的高中生在看到这则新闻以及 LLM 对数学不可否认的影响后，可能会有不同的看法。随着时间推移，强大的自动形式化工具应该能彻底消除上述痛苦，一旦我们将人类证明转换为 Lean 等语言的信心达到编译器将 Java 应用语言转换为字节码的水平。勘误可能永远存在，但在实践中，这些新方法将极大地提升严谨性并带来内心的平静。

（我对全新的发现则没那么有信心。有太多可能只是基于训练数据中的某些内容衍生出的发现，看似天才，实则只是在巨人的肩膀上小心翼翼地试探；而自动形式化对我来说绝对是令人信服的变革性技术，特别是用于检查 AI 输出证明的正确性时……）

“我们如此迅速地生成这一证明，表明现在已有可能对数学的大部分内容进行形式化，这既能捕捉现有数学证明体系中的错误，也能减轻审稿新工作的负担。”

^ 我觉得这段话应该放在前几段里。解释为什么这件事很重要，不应该被放在这么靠后的位置。

“这个证明并非我本人正在形式化的现代证明（该证明遵循 Khare、Taylor 等人的思路），而是 Darmon–Diamond–Taylor 在 1995 年对 Wiles–Taylor–Wiles 论证的阐述，该论证通过 Langlands–Tunnell 定理和 Ribet 的降阶定理展开。Anthropic 的仓库开发了 Fontaine 理论（用于研究伽罗瓦表示的平坦形变），并开发了足够的 Mazur 关于艾森斯坦理想的工作，从而得出结论：没有 Frey 曲线能拥有阶数 p>=17 的点。这意味着他们的 FLT 证明仅适用于 p>=17，不过 Best-Birkbeck-Brasca-Rodriguez 已经完成了奇正则素数的 FLT 形式化，而最小的不规则素数是 37，所以一切都没问题。”

我想问任何正在阅读此处的数学家：上面这段话对你来说有任何意义吗？

我之所以这么问，是因为我能读懂大部分与计算机工程、编程、硬件规格等相关的技术材料。即使我不完全理解所有细节，我也能很好地跟进。所以我想知道，专业数学家看到上述内容时，是否也能像资深软件工程师看懂计算机相关内容那样理解它。

“在此过程中，它编写了 1300 万行 Lean 代码，并证明了 29,500 个中间定理。”

简直疯了。我想这进一步证实了一个观点：任何能被证明是正确的东西，模型都能做到。

“一个智能体团队在不到两周的时间内完成了证明，消耗了约 60 亿个输出 token，使用的是一个通用内部研究模型，其能力大致相当于 Claude Fable 5.1。”

按每百万输出 token 50 美元计算，按 API 费率算，成本大约在 30 万美元左右（外加一点输入/预填充 token 的费用）。

顺便提一句，我强烈推荐 Simon Singh 写的这本书。

https://en.wikipedia.org/wiki/Fermat's_Last_Theorem_(book)

1300 万行代码，我们确定它没有利用 Lean 证明系统中的任何潜在漏洞吗？

随着 AI 工具的扩展，我们将越来越多地看到此类公告。虽然智能体编程令人印象深刻，但与医学、数学和物理研究的价值主张相比，它简直相形见绌。

我乐观地期待，在我有生之年，得益于 AI 的努力，我们将见证全球“万能药”的诞生：具有成本效益的大规模基因工程、治愈所有疾病的方法，甚至可能是治愈衰老的方法。

未来既美好又令人恐惧。

嗯，有点好笑。几年前有人声称 LLM 能做数学，我回复说如果它能证明费马大定理就好了：

https://news.ycombinator.com/item?id=33176996#33177939

> 现在试着让计算机证明：不存在自然数 a,b,c，使得对于任何 n > 2，都有 a^n + b^n = c^n。

> > 稍微有点移动球门柱了吧？

我想球门柱确实移动了一点，而且速度还挺快。