文章核心观点 - 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]

文章核心观点 - 数学家Boaz Klartag通过复兴并改进一种被放弃的几何方法，在任意高维空间的球体填充问题上取得了突破性进展，其新方法的填充效率实现了自1947年以来最显著的提升，并重新引发了关于最优填充性质（有序vs无序）的学术讨论[4][5][23][24] 数学问题与历史背景 - 球体填充问题旨在高效地将球体塞进高维盒子，在密码学、远程通信等领域有重要应用[1] - 开普勒在17世纪初证明三维球体最优排列可填满约74%的空间，但该猜想花费近400年才被证明[2] - 在更高维度（除8维和24维外），最优填充方式仍不明确，且过去的改进规模小、相对罕见[3] - 1905年，赫尔曼·闵可夫斯基建立了通过“格”来思考球体填充的直观方法[6] - 1947年，克劳德·安布罗斯·罗杰斯提出了从椭圆体开始构建球体填充的不同几何方法，但因其复杂性，数学家们后来回归并专注于闵可夫斯基的格理论方法[8][10][12] 研究方法与突破 - Klartag采用了一种基于随机过程演化椭球体的新方法，通过沿椭球体每个轴随机扩展和收缩边界，并在触及格点时冻结该方向的生长，从而“探索”并最大化空间[18] - 该方法经过调整后，被证明能产生足够大的椭球体，从而在转化为球体填充时创造新纪录[20] - Klartag仅用几个月的研究和几周的证明就取得了这一核心突破，其成功归因于他将凸几何的专业知识应用于这一长期停滞的领域[17][22][24] 研究成果与影响 - Klartag的新方法在转化为球体填充后，实现了自罗杰斯1947年论文以来最显著的效率提升[23] - 对于给定维度d，新方法可填充的球体数量是大多数先前结果的d倍，例如在100维空间中可填充约100倍的球体，在百万维空间中可填充约100万倍的球体[23] - 该成果重新引发了关于高维最优填充性质的争论：一些数学家曾认为需要更多无序性，但Klartag的工作支持了有序和对称可能才是最终出路的观点[24][25] - 关于填充密度是否已接近最优存在争议，但该突破对密码学和通信领域的潜在应用至关重要，并激发了相关领域研究人员的初步热情[26]