AI Agent Gauss一周内独立形式化菲尔兹奖级数学成果，20万行Lean代码公开
内容评分
摘要
AI Agent Gauss在短短一周内独立完成了2022年菲尔兹奖得主Maryna Viazovska关于8维和24维最优球体堆积问题的形式化证明。这项由Math Inc.开发的AI，仅用5天就完成了8维部分的验证，并在一周内生成了约20万行Lean代码，成为史上最大规模的单一目的Lean形式化项目。Gauss不仅大幅缩短了原需数月的工作量，还自主发现并修正了原论文中的细节错误，标志着AI在加速前沿数学研究方面达到里程碑式突破，被誉为“自动形式化领域的ImageNet时刻”。
正文
AI Gauss在短短5天内，完成了原本需要6个月才能完成的菲尔兹奖级数学成果的形式化证明。这一突破性进展在X平台引发了广泛讨论，有数学家将其誉为“自动形式化领域的ImageNet时刻”。
这项工作由Math公司开发的AI Gauss完成，具体是将Maryna Viazovska在2022年获得菲尔兹奖的成果——关于8维和24维最优球体堆积问题的定理——进行了形式化验证。这是本世纪以来首次有菲尔兹奖成果被完全形式化。Gauss的这项工作生成了约20万行Lean代码，使其成为历史上最大规模的单一目的Lean形式化项目。
值得关注的是，Gauss在推理验证过程中，还自主检测并纠正了原论文中的一处负号缺失和一处定义缺陷。
2022年，Maryna Viazovska因证明了E8晶格在8维空间中提供了最密堆积的相同球体，以及对相对极值问题和傅里叶分析问题的进一步贡献而获得菲尔兹奖。Gauss此次关注的正是其中的球体堆积问题。简而言之，该问题旨在证明在n维空间中，相同球体能达到的最高堆积密度。在更高维度上，这个问题极其复杂，直到Viazovska建立了该问题与模形式理论的创新性联系，利用傅里叶分析与模形式结合，构造优化辅助函数来严格验证E8晶格在8维空间中的最优性，并与合作者进一步证明了Leech晶格在24维空间中的最优性。
2024年，Viazovska及其合作者启动了这项成果的形式化项目。形式化是将数学证明严格表达为符合形式逻辑规则的形式语言，可由计算机验证，以提高数学的严谨性、可靠性和透明度。2025年11月，Gauss开始参与项目，在证明了若干模形式、径向施瓦茨函数和基础球体堆积理论问题后，其目标转变为自动完成项目的全部剩余工作。
项目进展远超预期：在前两年，人类专家团队共编写了约2万行Lean代码。而Gauss仅用5天时间，就新增约5万行代码，在没有借助额外辅助框架的情况下，完成了该问题的8维情形验证。团队原本估计，用现有工具完成这一项目还需6个月时间。随后，Gauss又花了一周时间，在研究了Viazovska原论文和20多篇额外参考文献后，生成了45万行代码，完成了24维情形的形式化证明。
Gauss的开发团队强调，Gauss是“独立推演了全部证明过程”。他们认为，对菲尔兹奖级别数学成果的验证表明，以Gauss为代表的AI，已经具备加速数学前沿研究发展的能力。扩大自动形式化的规模，将通过使全部已知数学成果变得可检索，彻底变革数学知识体系和数学发现方式。为了提高可维护性，研究人员还利用Gauss自动重构和优化了代码，将代码行数从峰值的50万行压缩到约20万行。所有代码均已在GitHub上发布。
Gauss的开发公司Math Inc.由xAI联合创始人、BatchNorm作者Christian Szegedy于2025年创办，致力于用AI“解决数学，解决一切”。此前，Gauss曾因用3周时间形式化陶哲轩和Alex Kontorovich提出的强素数定理（PNT）而声名鹊起。陶哲轩本人也与Math公司有所合作。正如Christian Szegedy所说，不到两年前，数学家们还认为AI要达到协助完成此类数学形式化工作的水平尚需多年，但“硅基高斯”今天已带来了最新突破。