IEEE：AI用五天验证了菲尔兹奖级别的数学证明，数学家们震惊了

一个困扰人类数学家近十年的验证任务，被一个AI在五天之内完成了。

这不是科幻小说，而是2025年底到2026年初真实发生的事情，而且主角是数学界最高荣誉菲尔兹奖背书的证明。

从一次偶遇开始的漫长旅程

故事要从2022年说起。那一年，乌克兰数学家玛丽娜·维亚佐夫斯卡获得菲尔兹奖，得奖原因是她解决了一个困扰数学界多年的高维球体堆积问题。

球体堆积问题听起来像是小孩子玩积木，但在高维空间里，它极其深刻，而且有非常实际的应用价值，包括智能手机和太空探测器使用的纠错码，都与球体能够多密集地填充空间这个数学问题直接相关。

维亚佐夫斯卡的贡献是证明了：在8维空间中，一种叫做E₈的对称排列是最优球体堆积方案，而在24维空间中，被称为Leech晶格的结构是最优解。这两个证明被数学界验证为正确，并最终带来了菲尔兹奖。

但数学界有一个比人工验证更严格的标准，叫做形式验证，即证明能被计算机系统以完全自动化的方式逐步核查，每一个推理步骤都无懈可击。这是另一个量级的挑战。

2024年3月，在瑞士洛桑，一次偶然的相遇改变了这个故事的走向。当时还是本科三年级学生的西达尔特·哈里哈兰，在校园里偶然遇到了维亚佐夫斯卡本人。哈里哈兰告诉她，自己一直在用形式化证明的方法来深入理解数学，维亚佐夫斯卡当场表示出了好奇和兴趣。

就这样，一个叫“精益形式化球体填充”的项目诞生了。

“精益”是一种编程语言，也是一种证明助手，允许数学家把证明写成代码，然后由计算机完全自动地验证其正确性，不存在任何人为判断的空间。项目团队逐步汇聚了来自帝国理工学院、东英吉利大学、加州大学伯克利分校等机构的数学家。他们的工作方式是先建立一份详细的“蓝图”，把8维证明的所有组成部分拆解标注，然后逐一补全缺失的形式化部分。

这项工作推进了整整15个月。

AI介入，五天完成人类需要几年的工作

2025年10月底，一家名为Math, Inc.的AI初创公司联系了哈里哈兰的团队。

这家公司正在开发一个叫高斯的AI系统，专门为数学形式化设计。高斯不是普通的大语言模型，它是一种推理代理，能够交织自然语言推理和完全形式化的机器推理，可以检索文献、调用工具、编写精益代码、启动验证编译器，像一个真正理解数学的工程师一样工作。

Math, Inc.告诉哈里哈兰，高斯已经自动完成了30个中间命题的证明，这些都是球体填充项目蓝图上标记的待解决事项。其中一个甚至帮助团队发现并修正了项目代码中的一处拼写错误。

但随后，沟通中断了。Math, Inc.似乎暂时失去了兴趣。

原来，他们正在悄悄升级高斯。

2026年1月中旬，新版高斯完成了一次内部测试：将数论中著名的质数定理的精益形式化，在两到三天内重现了旧版高斯需要三周才能完成的工作量。这个结果让Math, Inc.意识到，是时候回到球体填充问题了。

几天后，他们把新版高斯指向了哈里哈兰团队积累的蓝图和代码库。

结果震惊了所有人：高斯在五天之内，完成了8维球体填充证明的完整形式验证，包括修正发表论文中的拼写错误，总代码量超过20万行。

“当他们在一月底联系我们说已经完成时，委婉地说，我们非常惊讶，”哈里哈兰说，他现在已经是卡内基梅隆大学的博士生。

但这还不是故事的终点。

仅仅两周之后，Math, Inc.宣布高斯完成了更艰巨的任务：24维球体填充证明的完整形式验证，同样超过20万行代码，而且这一次没有现成的蓝图可以参考，所有必要的背景材料都需要高斯自己在线化补全。

普林斯顿大学的AI推理专家利亚姆·福尔，在了解这些结果后评价称：“这些新结果看起来非常非常令人印象深刻，确实预示着在这方面取得了快速进展。”

这意味着什么

形式验证在数学界被称为“橡皮图章”，但这个比喻低估了它的价值。它意味着一个证明不再只是数学共同体的集体判断，而是被机器以最严格的逻辑标准逐行审查，不存在任何模糊地带。

此前，形式验证的成本极高，需要大量人工将数学证明翻译成机器可读的代码，往往比写出原始证明耗费更多时间。正因如此，即便是获得菲尔兹奖的证明，也可能在很长时间内停留在“数学家们认为正确”的状态，而非“机器验证为正确”的状态。

高斯展示的能力，是把这个成本压缩了几个数量级。

Math, Inc.的CEO Jesse Han认为，这代表着数学实践方式的根本性变革的开端，极大规模的形式化将成为常态。他用了一个类比：程序员曾经是给卡片打孔的人，但后来编程语言把程序员从繁琐的底层操作中解放出来，让他们真正专注于解决问题本身。

“这类技术的最终结果，将是让数学家自由发挥他们最擅长的事，梦想新的数学世界。”

哈里哈兰和他的团队并没有因为AI接手了大量工作而感到被取代。他们强调，人类建立的蓝图、积累的代码库、以及与AI团队的持续协作，是整个成果的基础。

这次验证的真正意义，或许不在于AI有多强，而在于人类与AI的协作模式，第一次在数学这个最严谨的领域里，展示出了真实的生产力。

信息来源：https://spectrum.ieee.org/ai-proof-verification