5 天时间，AI 就搞定了原本需要 6 个月完成的菲尔兹奖级数学成果的形式化证明。
这一最新成果一经公布，立即在 x 上引发了讨论热潮，甚至有数学家称之为 "自动形式化领域的 ImageNet 时刻"。
这是本世纪以来首次有菲尔兹奖成果被完全形式化。
而单一项目 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 个月时间。
在完成证明的过程中，它还发现并修正了原论文的细节错误：在 Prop 7 中，函数 b ( t ) 的计算缺了一个负号，另外还有某处定义存在缺陷。
该研究团队认为：
对菲尔兹奖级别数学成果的验证表明，以 Gauss 为代表的 AI 智能体，已经具备加速数学前沿研究发展的能力。
扩大自动形式化的规模，将通过使全部已知数学成果变得可检索，彻底变革数学知识体系和数学发现方式。
p.s. 为了让这些形式化知识更加可维护，研究人员们还利用 Gauss 自动重构、优化改进了代码，把代码行数从峰值的 50 万行，压缩到了约 20 万行。
代码均已在 GitHub 上发布。
关于 Gauss
Gauss 背后公司 Math Inc. 的创始人，是 xAI 联合创始人、BatchNorm 作者 Christian Szegedy。
他在 2025 年创办 Math，致力于用 AI" 解决数学，解决一切 "。
而陶哲轩本人也和 Math 有所合作，将解析数论中的显式估计形式化，把依赖大量计算的论证转化为经过验证、可复用的构建模块。
在当时，外界对于 Gauss 这样的 AI Agent，还有许多质疑，包括自动化的程度、对数学问题隐含目标的忽略……但现在，正如 Christian Szegedy 自己所说：
（不到两年前）数学家们还认为，人工智能要达到能够协助完成此类数学形式化工作（菲尔兹奖级数学成果形式化）的水平，尚需多年。
参考链接：
[ 1 ] https://x.com/mathematics_inc/status/2028542388717986135
[ 2 ] https://www.math.inc/sphere-packing
— 欢迎 AI 产品从业者共建 —
「AI 产品知识库」是量子位智库基于长期产品库追踪和用户行为数据推出的飞书知识库，旨在成为 AI 行业从业者、投资者、研究者的核心信息枢纽与决策支持平台。
一键关注 点亮星标
科技前沿进展每日见
