这一最新成果一经公布立即在x上引发了讨论热潮甚至有数学家称之为“自动形式化领域的ImageNet时刻”。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上发布。关于GaussGauss背后公司Math Inc.的创始人是xAI联合创始人、BatchNorm作者Christian Szegedy。他在2025年创办Math致力于用AI“解决数学解决一切”。此前Gauss就因为用3周时间完成陶哲轩和Alex Kontorovich提出的数学挑战——在Lean中形式化强素数定理Prime Number TheoremPNT而一炮成名。而陶哲轩本人也和Math有所合作将解析数论中的显式估计形式化把依赖大量计算的论证转化为经过验证、可复用的构建模块。在当时外界对于Gauss这样的AI Agent还有许多质疑包括自动化的程度、对数学问题隐含目标的忽略……但现在正如Christian Szegedy自己所说不到两年前数学家们还认为人工智能要达到能够协助完成此类数学形式化工作菲尔兹奖级数学成果形式化的水平尚需多年。但“硅基高斯”在今天已经带来最新突破。