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万行。

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

但这还不是故事的终点。