5天搞定菲尔兹奖成果形式化！AI Agent刷新数学验证新纪录

Math公司研发的Gauss AI Agent仅用5天，完成了菲尔兹奖得主Maryna Viazovska 2022年获奖的8维、24维最优球体堆积定理的形式化验证，生成20万行Lean代码，成为史上最大规模单一目的Lean形式化项目，还自主纠正了原论文的一处错误，被学界称为自动形式化领域的ImageNet时刻。

2026年3月，一则来自数学AI领域的消息迅速席卷全球社交平台：一款被学界称为“硅基高斯”的AI Agent仅用5天时间，便完成了原本需要6名顶尖数学家耗时半年才能完成的工作——形式化验证2022年菲尔兹奖得主Maryna Viazovska的核心研究成果。这一成果不仅刷新了数学形式化验证的效率纪录，更引发了全球学界的广泛讨论。

形式化验证是将数学定理转化为计算机可自动校验的代码的过程，此前顶尖团队完成一项菲尔兹奖级成果的形式化验证，往往需要数月甚至数年的专注投入。而Gauss AI Agent仅用5天，就完成了对Maryna Viazovska 2022年菲尔兹奖获奖成果——8维与24维最优球体堆积定理的完整形式化验证。这也是本世纪以来，首次有菲尔兹奖级数学成果被完全形式化验证。

本次验证工作采用了目前主流的形式化验证编程语言Lean，Gauss共生成了超过20万行Lean代码，成为历史上规模最大的单一目的Lean形式化项目。目前，这批代码已全部公开，全球的数学家与AI开发者均可调用参考，为后续的数学形式化研究提供了重要的基础资源。