2026年3月，Math公司开发的AI Agent Gauss在一周内独立完成了菲尔兹奖级数学成果的形式化验证，涉及Maryna Viazovska在8维和24维最优球体堆积问题上的研究。这一成果原需6个月完成，现生成20万行Lean代码，成为历史上最大规模的单一目的形式化项目。Gauss还检测并修正了原论文中的细节错误，展示了AI加速数学研究的能力。团队认为，自动形式化将彻底变革数学知识体系。目前代码已公开发布。