AI 竟在 11 天内证明了 300 年未解的数学难题？

想象一下：您正在挑战破解一个 300 年来无人能解的古代密码。有人为此申请了政府资助，进行了长达 5 年的艰苦研究。然而突然间，AI 出现了，并宣布仅用 11 天就破解了这个密码。您会作何感想？

AI 公司 Anthropic 最近发布的消息正是这种情况。他们的 AI 模型“Claude”以计算机可验证的形式完全证明了数学界的巨大难题——“费马大定理（Fermat’s Last Theorem, FLT）”[出处 1, 13, 15]。

为什么这条新闻如此重要？

让 AI 在日常生活中“整理邮件”和让它解决数学难题是截然不同的两回事。数学证明是一项极其严苛的工作，不允许存在哪怕一行逻辑错误。

AI 不仅仅擅长写作，还能自主构建并验证复杂的数学逻辑，这意味着 AI 的“思维方式”已经进化到了一个新的阶段。这是一个强有力的信号：我们正在迎来一个 AI 可以比人类更快、更准确地辅助解决复杂科学计算和逻辑问题的时代 [出处 15]。

轻松理解：数学证明与“Lean”

在这里，我们要问：数学家所说的“证明”是什么？简单来说，这就是创建一个“任何人都无法反驳的完美说明书”的过程。过去，人类是在纸上书写并审核，而现在则是一个通过使用计算机可以理解的语言书写，并从机械层面确认其无误的时代。此时所使用的工具就是名为“Lean（一种辅助计算机验证数学证明的工具）”的编程语言 [出处 1, 3, 13]。

打个比方，“费马大定理”就像拼凑数千块拼图。数学家们绘制了拼图的大轮廓，而 Claude 则以极快的速度填补了符合这一图景的拼图碎片 [出处 4, 13]。

Claude 的这一成果再次提醒我们，数学证明是多么困难且漫长的过程。凯文·巴扎德（Kevin Buzzard）教授甚至为此申请了 5 年的研究资助，旨在将该定理形式化，而 Claude 则在 11 天内“在很大程度上自主（largely autonomously）”完成了这项工作 [出处 4, 13]。

现状：完全征服还是共同研究？

然而，数学界看待这一新闻的眼光有些复杂。尽管 Anthropic 宣布 Claude 独立解决了这个问题，但数学社区表示，很难说这一结果是“AI 独自完成的”[出处 7, 12]。

因为全世界的数学家们多年来一直为了拼好这幅拼图而共同努力，Claude 的成果很大程度上也是建立在这些基础之上的。事实上，费马大定理的形式化仍然是一个正在进行中的社区联合项目，学术界也有不少呼声，认为不应将此结果视为首个被形式化的证明 [出处 7]。

换句话说，AI 就像是一位在人类数学家数百年来积累的知识桥梁上飞速奔跑的运动员。尽管速度快得多，但那座桥梁本身依然是人类所建造的 [出处 9, 10]。

未来将走向何方？

未来，AI 与数学的邂逅将会更加频繁。这一结果已作为 Apache 2.0 协议开源，供所有人使用 [出处 5]。现在，AI 不仅仅是一个总结问题的秘书，它已经开始展现出成为人类未能解决的科学难题的“共同研究者”的潜能。

我们将与 AI 一起以更快的速度实现复杂的科学发现。AI 作为人类的智力工具，终将成为探索人类尚未触及的知识疆域的指南针，这一天已经不远了。

MindTickleBytes 的 AI 记者视角

AI 显然极大地提升了解决难题的速度，但数学的本质在于寻找答案的过程本身。这一案例表明，AI 可以成为扩展人类智力极限的强大工具。期待未来 AI 与人类数学家能够以某种方式合作，共同开拓更广阔的知识世界。

参考资料

1. [FLT: Anthropic has beaten me to it

   Xena](https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/)

2. [Formalizing Fermat’s Last Theorem

   Anthropic](https://www.anthropic.com/research/formalizing-fermats-last-theorem)

3. Techmeme: Anthropic says Claude worked “largely autonomously”…
4. GitHub - anthropics/fermats-last-theorem · GitHub
5. Fermat’s Last Theorem – from Wolfram MathWorld
6. Fermat’s Last Theorem in Lean: The Community… - DEV Community
7. ‘Amazing’ Math Bridge Extended Beyond Fermat’s Last Theorem
8. Proving Fermat’s last theorem: 2 mathematicians explain how building…
9. Fermat’s Last Theorem - Wikipedia
10. Claude helps complete first formalized proof of Fermat’s Last Theorem

11. [Learning more about Claude’s mathematical capabilities

    Anthropic](https://www.anthropic.com/research/riemann-zeta)

12. Lisan al Gaib on X: “Anthropic just uploaded a Lean 4 proof for Fermat’s last Theorem”
13. Anthropic Says Claude Produced Full Proof of Fermat’s Last Theorem, Verified With Lean