数学证明进入机器验证时代？

数学家安德鲁·怀尔斯于1995年发表了费马大定理的证明。图片来源：英国《自然》网站

费马大定理是过去半个世纪最著名的数学成果之一。9月4日，人工智能（AI）公司Anthropic宣布，其Claude模型仅用11天，就将英国数学家安德鲁·怀尔斯1995年完成的费马大定理证明转化为计算机可逐步验证的形式化证明。

“机器竟然能够把人类数学家的工作转化为一份长达1300万行、坚不可摧的证明，这完全让我震撼。”美国罗格斯大学数论学家亚历克斯·孔托罗维奇说。

英国《自然》网站在7日发表的文章中称，这一成果表明，AI将在数学家的工作中发挥越来越重要的作用，不仅可帮助检验数学证明，也可能参与产生新的数学推理。按照目前的发展速度，AI审查整个人类数学知识库，已不再是遥不可及的事，甚至可能发现一些广为人知的数学结论中是否藏着错误。而在两年前，这还只是幻想。

AI打破人工核验局限

数学证明是一连串严密的逻辑步骤，只要其中一环出错，整个证明就可能坍塌。面对动辄数百页、涉及大量复杂理论的证明，单靠人工逐一核验每个环节，几乎是不可能完成的任务。

费马大定理就是一个典型。1637年，法国数学家皮埃尔·德·费马提出了这个命题：当整数n大于2时，不存在满足xn+yn=zn的正整数x、y、z。

1908年，德国曾悬赏一笔奖金（今天约合100万至200万美元），向数学家征集费马大定理的证明。仅第一年，就收到了621份证明，但没有一份站得住脚。直到上世纪90年代，英国数学家安德鲁·怀尔斯才真正攻克了这一难题。他在1995年5月发表了长达129页的证明，横跨数论多个分支，汇集了大量现代数学成果。该证明通过了数学界审查并得到认可，费马大定理就此尘埃落定。

所谓“形式化”证明，就是把数学证明翻译成一种极其严格、精确的语言，让计算机能够自行验证其中的每一步，而不需要依赖人的主观判断。

近年来，AI进行数学形式化的能力进步很快。今年2月，AI辅助数学形式化取得一项里程碑式进展，成功对菲尔兹奖得主玛丽娜·维亚佐夫斯卡关于8维和24维空间中最有效球体堆积方式的研究成果完成了计算机验证。不过，英国伦敦帝国理工学院数学家凯文·巴扎德说，费马大定理的形式化工作“可能更困难一个数量级”。

预估十年工作量被AI压缩到11天

2024年，巴扎德启动了一个项目，目标是把怀尔斯的证明翻译成Lean语言，以便计算机验证。他原本估计这项工作需要10年。项目自身的规划文件就长达86页，资金支持目前已经确定到2029年。

一年多后，AI大大推进了工作进度。Anthropic让Claude承担了费马大定理的形式化任务。据Anthropic介绍，哥伦比亚大学研究人员彭天翼及其团队让数十个Claude智能体并行工作，不同智能体分别负责定义数学概念、证明较小的辅助定理，再将这些结果逐步组合起来。

Claude此次使用的Lean是一种专门用于形式化数学的证明辅助工具。数学家通过Lean把数学定义、定理和推理写成计算机能够处理的形式，再由计算机检查证明过程。

与Lean配套的Mathlib是一个由数学家持续维护的数学代码库，其中已经收录了大量经过形式化处理的数学知识。新的数学证明可以调用其中已有的定义和定理，从而避免重复劳动。

不过，这项工作最初并不顺利。智能体会忘记其他智能体已经完成的工作，产生重复工作，有时甚至停止协作。研究团队随后使用Prove2Me工具，为智能体提供实时任务清单，记录已完成和待办事项，帮助各智能体调用已有成果。

经过11天运转，Claude完成了整个形式化过程，证明了约3万个辅助定理，生成了约1300万行代码，规模相当于160部长篇小说。

正确判定率从99.9%到100%

经过形式化之后，怀尔斯的证明获得了一份计算机可逐行核验的“认证”。巴扎德说，过去自己有“99.9%的把握”认为这份证明正确，如今则是“100%”。

这种确定性对于数学同行评审尤为关键。数学论文数量不断增加，篇幅越来越长，涉及的数学知识也愈加复杂，人工检查一份完整证明往往需要耗费大量时间。即使如此，仍可能漏掉一些错误。

数学家对这种情况并不陌生。开普勒猜想的一项计算机辅助证明花了4年时间，之后审查小组仍只能给出“99%确定”的评价。格里戈里·佩雷尔曼关于庞加莱猜想的证明，也花费了大约4年时间才得到数学界充分理解和认可。

美国加州大学圣迭戈分校数学家弗雷德里克·曼纳斯设想，如果有一种“魔法”，能够把一篇发表在预印本平台arXiv上的论文交给机器，由机器判定证明是否正确，或者直接指出其中错误，那将具有极其重要的价值。

如今，Claude生成的约1300万行证明已经公开在GitHub上，任何数学家都可以免费获取并逐行核查。随着AI参与数学形式化的能力不断提升，曼纳斯设想的“魔法”正从想象一步步走向现实。（记者 张佳欣）