在短短五天内，AI成功完成了原本需要六个月才能完成的数学定理的形式化证明工作。
这一成就一经公布便迅速在社交媒体上引发了广泛讨论，甚至有专家将其形容为“形式化领域的ImageNet时刻”。
该成果由Math公司研发的人工智能Gauss实现。具体而言，它完成了对Maryna Viazovska于2022年因解决8维和24维度球体堆叠问题而获得的菲尔兹奖数学成就的形式化验证工作。
这项研究是本世纪以来首次将菲尔兹级数学成果进行完全形式化的尝试。
此次项目中，“硅基高斯”生成了超过二十万行Lean代码，成为历史上规模最大的单一目标Lean形式化工程之一。
另一个值得一提的是，在验证过程中，Gauss还自主发现了并纠正了原论文中的错误。
2022年时，Maryna Viazovska因其在8维空间中证明E8晶格具有最优球体堆叠的特性及对相关极值和傅里叶分析问题的研究贡献而获得菲尔兹奖。
其中提到的维度堆叠问题正是此次Gauss研究的重点对象之一。
简单来说，就是在不同维度下，相同大小的球体能以多大密度进行排列的问题。
一维和二维的情况相对简单且早有定论。而三维情形则在开普勒于1611年提出猜想后，直到1998年才由数学家Thomas Hales借助计算机辅助完成证明；其形式化验证又耗费了十余年的努力。
在更高维度上，问题变得更加复杂和难以攻克。直到Maryna Viazovska找到了这个与模形式理论之间的联系，并创新性地结合傅里叶分析方法进行研究。
她通过构造一种优化的辅助函数，严格验证了E8晶格在八维空间中的最优特性。
同样基于这种方法，她和合作者还证明Leech晶格提供了二十四维度空间中球体堆叠的最大密度。
2024年起，Maryna Viazovska及其团队开始着手推动这一成果的形式化工作。
形式化是指将数学证明转换为符合形式逻辑规则的语言表达。这样可以确保每一步都遵循严格的逻辑规范，并提高数学的严谨性、可靠性和透明度。
2025年十一月，“硅基高斯”开始参与这项工作，在解决了若干关于模形式和球体堆叠理论的问题后，它设定了自动完成剩余工作的目标。
随着事情的发展逐渐超出人们的预期：
在过去的两年中，人类专家团队总共编写了约两万行Lean代码。而Gauss仅用了五天时间就新增了大约五万行代码，在没有额外辅助框架的情况下完成了八维情形的验证。
之前的人类专家估计完成这项工作仍需要六个月的时间。
接下来的七天里，Gauss通过研究Viazovska原始论文和超过二十篇相关文献，生成了四十五万行代码，成功解决了二十四维度的情形形式化证明问题。
Gauss背后的团队强调，该AI独立推导出了整个证明过程。
在完成验证的过程中，它还发现并修正了原论文中的细节错误：在Prop 7中，函数b(t)的计算缺少了一个负号，并且某处定义存在缺陷。
该研究团队认为：
这表明以Gauss为代表的AI智能体已经具备加速数学前沿研究发展的潜力。扩大自动形式化的规模将彻底改变数学知识体系和发现方式。
为了保持这些形式化知识的维护性，研究人员利用Gauss优化和改进了代码，将峰值时五十万行代码压缩到了约二十万行。
相关代码已在GitHub上公开发布。
Gauss背后的Math公司由xAI联合创始人、BatchNorm作者Christian Szegedy创立于2025年。
他创办该公司，致力于通过AI“解决数学，解决一切”。
在此之前，Gauss因其用三周时间完成陶哲轩和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
— 完 —