文章核心观点 - AI（Math公司的Gauss）在极短时间内完成了对菲尔兹奖级数学成果的形式化证明，这标志着自动形式化领域取得了重大突破，被类比为“ImageNet时刻”，预示着AI将彻底改变数学知识体系和发现方式 [1][2][19][27] AI成就与技术突破 - **效率突破**：Gauss仅用**5天时间**完成了原本需要**6个月**才能完成的8维情形形式化验证，新增约**5万行**Lean代码 [16][17] - **规模突破**：整个项目（8维和24维）最终生成约**20万行**Lean代码（经优化后），是历史上最大规模的单一目的Lean形式化项目 [6][20] - **能力突破**：AI在推理过程中自主检测并纠正了原论文中的细节错误（如Prop 7中函数b(t)计算缺负号），证明了其独立推演和验证复杂证明的能力 [7][18] - **连续突破**：在完成8维证明后，Gauss又用**一周时间**，研究了原论文和**20+篇**参考文献，生成**45万行**代码（峰值），完成了24维情形的形式化证明 [17][20] 项目背景与数学意义 - **证明对象**：形式化验证了Maryna Viazovska在2022年获得菲尔兹奖的成果，即关于**8维和24维最优球体堆积问题**的定理 [4][8] - **问题难度**：高维球体堆积问题极为复杂，三维情形的证明（1998年）及其形式化验证就耗费了十余年，Viazovska的创新方法（结合傅里叶分析与模形式）是解决8维和24维问题的关键 [10][11] - **历史意义**：这是**本世纪以来首次**有菲尔兹奖成果被完全形式化 [5] - **项目历程**：人类专家团队在前两年编写了约**2万行**代码，Gauss于2025年11月加入项目并最终主导完成了剩余全部工作 [15][16] 公司及AI产品（Gauss）背景 - **开发公司**：Gauss由Math Inc.开发，该公司由xAI联合创始人、BatchNorm作者Christian Szegedy于2025年创立 [22][23] - **公司使命**：致力于用AI“解决数学，解决一切” [23] - **产品声誉**：Gauss此前已因用**3周时间**形式化了陶哲轩等提出的**强素数定理（PNT）** 而闻名，并与陶哲轩有合作项目 [25][26] - **代码开源**：本次菲尔兹奖成果的形式化代码已在GitHub上发布 [21] 行业影响与未来展望 - **能力认可**：验证表明，以Gauss为代表的AI智能体已具备加速数学前沿研究发展的能力 [18] - **变革潜力**：扩大自动形式化的规模，将使全部已知数学成果变得可检索，从而**彻底变革数学知识体系和数学发现方式** [19] - **超越预期**：此次突破远超数学家们两年前的预期，当时认为AI要达到协助完成此类工作的水平尚需多年 [26]