AI Agent搞定世纪首次菲尔兹奖成果形式化！一周时间独立完成，20万行代码已公开

鱼羊 发自 凹非寺 量子位 | 公众号 QbitAI 5天时间，AI就搞定了原本需要6个月完成的 菲尔兹奖级数学成果 的形式化证明。 这一最新成果一经公布，立即在x上引发了讨论热潮，甚至有数学家称之为" 自动形式化领域的ImageNet时刻 "。 AI是来自 Math 这家公司名为 Gauss 的AI。具体完成的工作，是形式化验证了让Maryna Viazovska在2022年获得数学最高奖——菲尔兹 奖的成果：关于8维和24维最优球体堆积问题的定理。 这是 本世纪以来首次有菲尔兹奖成果被完全形式化 。 而单一项目20万行Lean代码，也使得"硅基高斯"的这项最新工作，成为 历史上最大规模的单一目的Lean形式化项目 。 还有一个引起大家关注的重点是，"硅基高斯"在推理验证过程中，还自主检测并纠正了原论文中的错误。 在更高维度上，这个问题就更加复杂、难以攻克。直到Maryna Viazovska找出了该问题与模形式理论之间的联系—— 她利用一种创新的方法，将傅里叶分析与模形式结合起来，构造了一个优化的辅助函数来严格验证E 8 晶格在8维空间中的最优性。 基于同样的方法，她还和合作者们一起，进一步证明Leech ...