AI Agent搞定世纪首次菲尔兹奖成果形式化！一周时间独立完成，20万行代码已公开

5天时间，AI就搞定了原本需要6个月完成的菲尔兹奖级数学成果的形式化证明。

这一最新成果一经公布，立即在x上引发了讨论热潮，甚至有数学家称之为“自动形式化领域的ImageNet时刻”。

AI是来自Math这家公司名为Gauss的AI。具体完成的工作，是形式化验证了让Maryna Viazovska在2022年获得数学最高奖——菲尔兹奖的成果：关于8维和24维最优球体堆积问题的定理。

这是本世纪以来首次有菲尔兹奖成果被完全形式化。

而单一项目20万行Lean代码，也使得“硅基高斯”的这项最新工作，成为历史上最大规模的单一目的Lean形式化项目。

还有一个引起大家关注的重点是，“硅基高斯”在推理验证过程中，还自主检测并纠正了原论文中的错误。

本世纪首次完成菲尔兹奖成果形式化

2022年，Maryna Viazovska拿下菲尔兹奖的获奖理由是：证明了E8晶格在8维空间中提供了最密堆积的相同球体，以及对相对极值问题和傅里叶分析问题的进一步贡献。

其中提到的这个球体堆积问题，就是这次“硅基高斯”所关注的。

简单来说，就是要证明，在n维空间中，相同的球体最多能以多高的密度进行堆积。

在一维情形下，这个问题并不复杂，二维情形也早有证明。但当n的数字来到3，也就是在三维情形下，尽管开普勒在1611年就提出了相关猜想，但直到1998年，数学家Thomas Hales才在计算机的辅助下完成了证明；而三维情形的形式化验证，则又耗费了十余年的时间。

在更高维度上，这个问题就更加复杂、难以攻克。直到Maryna Viazovska找出了该问题与模形式理论之间的联系——

她利用一种创新的方法，将傅里叶分析与模形式结合起来，构造了一个优化的辅助函数来严格验证E8晶格在8维空间中的最优性。

基于同样的方法，她还和合作者们一起，进一步证明Leech晶格提供了24维空间中最密的球体堆积。

△AI生成

2024年，Maryna Viazovska开始和合作者们一起推动对这一成果的形式化项目。

形式化是指将数学证明严格地表达为符合形式逻辑规则的形式语言。这种过程可以被计算机验证，以确保证明的每一步都完全符合逻辑规则，主要目的是提高数学的严谨性、可靠性和透明性。

2025年11月，“硅基高斯”开始参与到这个项目之中。在证明了若干关于模形式、径向施瓦茨函数和基础球体堆积理论的问题之后，这个AI的目标变成了：自动完成该项目的全部剩余工作。

于是事情的发展开始超乎人们的想象：

在前两年，人类专家团队共编写了约2万行Lean代码。而Gauss仅用5天的时间，就新增约5万行代码，在没有借助额外辅助框架的情况下，完成了该问题的8维情形验证。

团队原本估计，用现有工具，要完成这一项目还需6个月时间。

又花了一周时间，Gauss在研究了Viazovska原论文和20+篇额外参考文献后，生成45万行代码，把24维情形的形式化证明也给搞定了。

“硅基高斯”背后团队强调，Gauss是“独立推演了全部证明过程”。

在完成证明的过程中，它还发现并修正了原论文的细节错误：在Prop 7中，函数b(t)的计算缺了一个负号，另外还有某处定义存在缺陷。

该研究团队认为：

对菲尔兹奖级别数学成果的验证表明，以Gauss为代表的AI智能体，已经具备加速数学前沿研究发展的能力。

扩大自动形式化的规模，将通过使全部已知数学成果变得可检索，彻底变革数学知识体系和数学发现方式。

p.s. 为了让这些形式化知识更加可维护，研究人员们还利用Gauss自动重构、优化改进了代码，把代码行数从峰值的50万行，压缩到了约20万行。

代码均已在GitHub上发布。

关于Gauss

Gauss背后公司Math Inc.的创始人，是xAI联合创始人、BatchNorm作者Christian Szegedy。

他在2025年创办Math，致力于用AI“解决数学，解决一切”。

此前，Gauss就因为用3周时间，完成陶哲轩和Alex Kontorovich提出的数学挑战——在Lean中形式化强素数定理（Prime Number Theorem，PNT），而一炮成名。

而陶哲轩本人也和Math有所合作，将解析数论中的显式估计形式化，把依赖大量计算的论证转化为经过验证、可复用的构建模块。

在当时，外界对于Gauss这样的AI Agent，还有许多质疑，包括自动化的程度、对数学问题隐含目标的忽略……但现在，正如Christian Szegedy自己所说：

（不到两年前）数学家们还认为，人工智能要达到能够协助完成此类数学形式化工作（菲尔兹奖级数学成果形式化）的水平，尚需多年。

但“硅基高斯”，在今天已经带来最新突破。

参考链接：

[1]https://x.com/mathematics_inc/status/2028542388717986135

[2]https://www.math.inc/sphere-packing

文章来自于“量子位”，作者 “鱼羊”。