AI是否“解决”了费马大定理？1300万行证明在11天内完成，改变数学

AI是否“解决”了费马大定理？1300万行证明在11天内完成，改变数学

11天内被“证明”的350年难题

数学史上最著名的难题之一再次引起了全世界的关注。

Anthropic于2026年9月宣布，其AI“Claude”完成了费尔马大定理的从头到尾可计算机验证的完整形式证明。整个过程耗时11天。生成的Lean代码约有1300万行，在过程中证明了3万300个定理，其中2万9500个用于最终证明。

单从这些数字来看，似乎AI在短短11天内解决了一个困扰人类数百年的难题。然而，这里有一个重要的区别。Claude所做的并不是发现未知的解法，而是将安德鲁·怀尔斯和理查德·泰勒在1990年代完成并被数学界认可的证明翻译成计算机可以逐步逻辑验证的语言，并填补了大量缺失的中间部分。

“不是发现新的证明”，而是“对现有证明的完整机器验证”。如果不理解这一点，成果就会被过高估计。另一方面，如果将形式化仅视为翻译工作，则会低估其难度和此次成果的震撼。


费尔马留在空白处的一行

费尔马大定理声称，对于正整数a、b、c和大于2的整数n，不存在满足“a的n次方＋b的n次方＝c的n次方”的整数解。

皮埃尔·德·费尔马大约在1637年，在古希腊数学书《算术》的空白处写下了这一主张，并表示找到了惊人的证明，但空白处太小，无法写下。然而，这个证明从未被发现。

此后，几代数学家不断挑战，虽然对个别指数的证明取得了进展，但一般情况下仍未解决，长达350多年。转折点在1993年，怀尔斯经过多年的秘密研究发表了证明，但在验证中发现了重大缺陷。怀尔斯与泰勒一起进行修正，并于1994年克服了问题。论文于1995年发表。

这个故事表明，数学中的“已证明”并不是有人写下答案的瞬间就成立的。证明必须被其他专家阅读，连同前提和引用的定理一起被审查，并确保逻辑链没有断裂。即使是像怀尔斯这样的数学家的证明，在首次发表后也发现了漏洞，这象征着其难度。


“对人类显而易见”的，对计算机却不通用

通常的数学论文是以人类专家为阅读对象撰写的。作者省略常识性变形，引用已知结果，并不明确说明从上下文可以理解的部分。读者也利用背景知识，补充行间逻辑。

然而，计算机不会推测“这里显而易见吧”。必须严格指定定义、前提、类型、使用的定理以及由此导出的结论，并证明每个阶段都遵循规则。用于这项工作的工具是定理证明辅助系统Lean。

在Lean中，证明以接近程序的形式描述。一个小型内核检查输入的证明是否符合逻辑规则，如果中途有飞跃则不予接受。从这个意义上说，形式证明类似于对数学主张的非常严格的自动测试。

困难在于，仅仅将怀尔斯的论文转换为机器语言并不能结束。面向人类的证明建立在代数、几何、调和分析、数论等庞大的知识体系之上。如果Lean的共享库中不存在所需的概念或辅助定理，则必须重新定义和证明它们。此次1300万行的规模，也是逐一构建这些“看不见的基础”的结果。


多个AI分工完成巨大的证明

在Anthropic的实验中，数十个Claude代理并行工作。一个代理定义概念，另一个代理证明辅助定理，还有其他代理将它们组合起来，进而推进到更高层次的定理。AI群体大规模地执行了类似于人类进行的合作研究的分工。

然而，一开始并不顺利。早期的尝试中，代理失去了对项目整体进度的把握，无法有效利用彼此的成果。在长期工作中，不仅个别AI的推理能力，而且管理哪些任务已完成、接下来应证明什么的机制至关重要。

为此，使用了将定理之间的依赖关系管理为有向无环图的共同形式化平台Prove2Me。将需要证明的项目像地图一样排列，使每个代理可以选择未解决的任务，并让其他代理可以重用完成的结果。Lean的编译负荷被抑制，自然语言的解释也可以用于搜索，这些设计支持了大规模的分工。

最终，AI群体消耗了约60亿个输出标记，在不到11天内到达了证明的根部。根据Anthropic的说法，除了Lean的检查外，还通过比较工具确认了定理的最终描述与现有库Mathlib中的费尔马大定理一致。也就是说，并不是证明了一个名字相似的不同问题，而是确认达到了预期的主张。


人类的5年计划与AI的11天无法简单比较

此次常被对比的是，由帝国理工学院的数学家凯文·巴扎德领导的人类中心形式化项目。该项目于2024年启动，计划用数年时间在Lean中形式化费尔马大定理。

“人类花5年时间的工作，AI在11天内完成”这一说法令人震惊，但两者的目标并不完全相同。Anthropic的成果优先确保定理从头到尾可被机器验证。而巴扎德等人则致力于整备可纳入共享库的基础理论，并创建人类可以探索现代证明并学习的动态文档。

在短时间内创建“通过”的巨大代码，与整理成数学家可以理解、再利用并连接到下一项研究的形式是不同的任务。Anthropic自己也解释说，他们利用了人类项目和现有Mathlib构建的基础。将此次竞争描绘为AI与数学家的简单速度竞赛并不准确。

即便如此，从头到尾的形式化不再需要以年为单位，而是以天为单位完成的事实意义重大。巴扎德在自己的博客中表示，尽管从这一成果中几乎没有得出新的数学内容，但AI群体在11天内形式化了相当于数千页的文献，这显示了自动形式化的可能性。他还表示，形式化后对原本认为99.9%正确的证明可以100%确信，这也被视为这一成果的象征。


社交媒体上分为“惊叹”和“这不是新发现”两派

发布后，X、Reddit、Hacker News等平台上引起了巨大反响。Lean官方账号将其作为首个完全计算机验证的证明介绍。在Hacker News上，相关帖子收集了数百条评论，Reddit上也有“几年前无法想象”“被1300万行的规模震撼”“需要超过2万9000个中间定理吗”等惊讶的声音接连出现。

 

另一方面，最常被重复的是对标题的理解的警告。针对“AI解决了费尔马大定理”这一表述，许多人纠正说“解决的是怀尔斯和泰勒，Claude是将现有证明形式化为Lean”“这不是新的数学发现”。反应中也有将形式化视为简单格式转换的意见，但对此也有反驳，认为补充长大证明缺失的基础，并使数万中间定理可被机器验证本身就是一项重大的研究成果。

讨论还涉及研究者的角色和资金分配。有人欢迎AI在短时间内达到以巨额资助和多年计划推进的工作的成就，视为研究生产力的飞跃。与此同时，也有人表达了对年轻研究者的主题可能被AI抢先，以及数学手工思考动机可能丧失的担忧。在巴扎德的博客评论区，也有“数学的悲惨终结”与“数学内容没有改变，只是验证手段进步了”的回应交锋。

这些并不是随机抽样的民意调查，而只是各社交平台上可见的帖子趋势。然而，这很好地展示了此次成果为何容易被误解，同时也引发强烈情感反应。人们反应的不仅仅是一个定理，而是“智力劳动的自动化能走多远”这一更大的问题。


正确的证明与有用的证明并不相同

此次成果也有明显的弱点。1300万行的规模超过了主要数学库Mathlib的5倍。即使机器可以确认其正确性，人类要掌握全貌、找到所需部分并在其他证明中再利用并不容易。

数学的发展不仅需要正确的结论，还需要能够理解为何如此的解释、整理概念的适当抽象化、可用于其他领域的引理。如果每次都将相同的基础理论作为巨大的专用代码重写，即使形式证明增多，知识体系也难以成长。尽管可验证的证明大量生产，但每个证明可能成为缺乏兼容性的孤岛。

因此，下一步的任务可能是将AI生成的代码简化整理，归还到Mathlib，并与人类可读的解释对应起来。AI粗略地开辟道路，人类和AI将这条路绘制成地图。此次成果更像是这一新分工的起点，而非终点。


补充审阅的极限，“不知疲倦的第二读者”

最大意义不在于再次证明了著名定理，而在于展示了以往因成本和时间而不切实际的机器验证可以大规模执行的可能性。

数学论文的验证需要专家的长时间投入。尤其是当新理论长达数百页，并依赖大量先行研究时，审阅者难以重构全部内容。如果AI可以辅助形式化，或许会普及与人类面向的论文一起提交可在Lean等工具中检查的证明书的习惯。

这在AI开始大量生成数学成果的时代尤为重要。如果AI生成的论文候选超过人类阅读速度，传统的审阅方式将难以应对。通过结合生成AI、形式化AI和最终由小型验证内核确认逻辑的机制，至少可以高效地确认“逻辑上是否得出结论”。

当然，形式证明并不能判定论文的全部价值。定义是否适当地表达了现实问题、研究课题是否重要、证明是否提供了新的洞察、解释是否具有教育性等判断仍然存在。此外，对验证软件和基础库的信任、巨大代码的审计、计算资源的不均等问题也无法避免。

即便如此，数学获得一个不知疲倦、不顾权威、不放过逻辑漏洞的“第二读者”的意义重大。


AI会取代数学家吗

此次事件并不是AI全面替代了数学家的工作。创造证明原型的人类、几十年整理论的研究者、培育Mathlib和Lean的社区、设计证明分割基础的开发者，共同成就了Claude的11天。

然而，“因此AI只是工具”这样的结论也为时过早。多个代理从失败中重建，追踪依赖关系，积累数万定理，完成巨大目标，这与传统自动化有质的不同。不是人类逐步细致命令，而是AI群体在给定目标和工作环境下，执行了长期项目的相当一部分。

未来，数学家的价值可能会从“手动编写证明代码的速度”进一步转向选择哪些问题、用哪些概念整理、解释结果意味着什么的能力。AI可以加速验证，但并不会自动完成将数学作为人类知识编辑的工作。

关于费尔马大定理本身，没有新的结论。怀尔斯和泰勒的证明是正确的。然而，将这种正确性以机器可以从头到尾验证的形式完成的工作在11天内完成，这一事实改变了数学的构建、阅读和信任方式。

费尔马未能写下的证明，约360年后，如今膨胀至1300万行。而下一个挑战可能是将这个庞大的证明再次压缩为人类可以理解的知识。


出处URL

相关文章