从358年悬案到11日验证❗️AI攻克数学史上最著名难题

美国人工智能公司Anthropic宣布了一项震动数学界的突破性进展：其AI模型Claude在基本自主运行11天后，完成了费马大定理（Fermat's Last Theorem）的首个端到端、可由计算机完整检查的形式化证明。这一成果被数学界视为AI在基础科学领域的重要里程碑。

据Anthropic披露，Claude在此期间写下了约1300万行Lean代码，共产出了约30300个可由计算机验证的定理，其中29500个中间定理进入最终证明。最终代码量已超过Lean核心数学库Mathlib的5倍以上，是迄今为止规模最大的Lean证明项目。整个项目消耗约60亿个输出Token，使用的是Anthropic内部一款能力大致相当于Claude Fable 5.1的通用研究模型。

这项工作的发起者是Anthropic研究员彭天翼（Tianyi Peng）。他本科毕业于清华大学姚班，博士毕业于麻省理工学院，现任哥伦比亚大学商学院助理教授。

多智能体协作，克服“失忆”难题

完成这项壮举的并非单个Claude模型，而是数十个Claude智能体（Agent）并行协作。它们各司其职：有的补充数学定义，有的专攻中间引理，有的向更高层定理推进，还有的负责将不同部分拼回完整的证明体系。

然而，起初并不顺利。Anthropic发现，当多个智能体直接协作时，它们很快开始“失忆”——忘记工程进行到哪里、无法复用彼此的结果，协作陷入停滞。转折点是团队引入了由彭天翼及其团队开发的Prove2Me平台。该平台将整个证明拆解为一个有向无环图（DAG），清晰记录每个定理及其前后依赖关系，让每个智能体都能看清全局进度、判断任务依赖。自此，协作得以高效推进。

数学家：从99.9%到100%的确信

自2024年以来，伦敦帝国理工学院的数学家Kevin Buzzard领导了一个专门针对费马大定理形式化的大型开源项目，预计需要10年才能完成。然而Claude在11天内就完成了自己的Lean认证。

Buzzard在审查了Claude的证明后表示：“以前，我有 99.9% 的把握认为该证明是正确的，在Claude的工作完成后，我现在是 100% 确信。”他还指出，按照当前的发展速度，AI或许不久就能审视整个数学知识库，甚至可能发现某些著名结论是错误的——两年前，这还是个幻想。

美国罗格斯大学数论学家Alex Kontorovich表示，AI能够将人类数学家的工作转化为长达1300万行的严谨证明，这一事实“令我大为震撼”。加拿大多伦多大学数论学家Daniel Litt评价道：“如果它能形式化费马大定理，那么它大概就能形式化任何东西。”

需要强调的是，Claude并非发现了一条全新的费马大定理证明路线，而是将数学家安德鲁·怀尔斯（Andrew Wiles）于1995年发表的129页人类证明，完整转写成了计算机能够逐行检查、没有任何逻辑跳步的形式化证明。

什么是费马大定理？

费马大定理（Fermat's Last Theorem），又称“费马最后定理”，是数学史上最著名的难题之一。

定理内容：当整数 n > 2 时，关于 x、y、z 的方程 xⁿ + yⁿ = zⁿ 不存在正整数解。

起源：1637年，法国数学家皮埃尔·德·费马（Pierre de Fermat）在一本古希腊数学家丢番图《算术》的书籍页边写下：“将一个高于二次的幂分解为两个同次的幂，这是不可能的。关于此，我发现了该定理的一个真正奇妙的证明，但书上空白的地方太少，写不下。”此后三百多年，费马口中那个“绝妙证明”成为数学界的终极谜题。

证明历程：欧拉、勒让德、库默尔等一代代顶尖数学家前赴后继，始终未能拿下完整证明。直到1993年，英国数学家安德鲁·怀尔斯公开宣布完成证明，但两个月后同行评审发现其中存在关键漏洞。怀尔斯又花了一年时间，与前学生理查德·泰勒（Richard Taylor）合作修补，最终于1995年正式发表了129页的完整证明。这一成果被公认为20世纪数学的里程碑。

费马大定理之所以著名，不仅因为其表述极其简洁——任何一个学过勾股定理的人都能理解——更因为其证明难度极高，跨越了358年才最终被攻克。如今，AI用11天完成了人类预计10年的形式化工程，为这段跨越四个世纪的数学传奇写下了新的篇章。

（新闻来源：🔗franceinfo）