菲尔兹奖成果首次被AI完整形式化，Gauss20万行代码改写数学史？

AI 在数学领域的研究取得新进展！ 近日，一家名为 Math, Inc. 的公司宣称利用 Gauss 智能体，已经完成了一个关乎 8 维和 24 维空间中的最优球体堆积定理的形式化证明，代码量约为 20 万行 （LOC）。 这一定理最初由数学家玛丽娜・维亚佐夫斯卡（Maryna Viazovska）及其合作者证明，Maryna Viazovska 也凭此荣获 2022 年国际数学家大会菲尔兹奖。 据悉， 这是本世纪唯一一个被完全形式化证明的菲尔兹奖成果，也是历史上规模最大的单一用途 Lean 形式化项目。 而背后的这家名为 Math, Inc. 的公司，也不是第一次完成数学问题的形式化证明了。 资料显示，Math, Inc. 是由 xAI 前联合创始人、Morph Labs 首席科学家 Christian Szegedy 创立，致力于通过自动形式化技术打造可验证超级智能，Gauss 则是首款 专为协助数学专家开展形式化验证工作打造的自动形式化智能体。 去年， Gauss 只用了三周时间，就完成了陶哲轩和 Alex Kontorovich 提出的数学挑战， 即在 Lean 定理证明器中完成强素数定理（Prime ...