---
title: Math, Inc. 称旗下 AI 系统 Gauss 完成 Viazovska 球堆积证明的 Lean 形式化
dek: Math, Inc. 于 2026 年 3 月表示，旗下 AI 系统 Gauss 已完成 Maryna Viazovska 8 维和 24 维球堆积证明的 Lean 形式化，这些证明曾为她赢得菲尔兹奖。8 维部分的工作有人类撰写的蓝图作指引，24 维情形则没有，因此后者的形式化命题最需要独立审查。
---
开发 AI 系统 Gauss 的初创公司 Math, Inc. 称，Gauss 协助完成了 Maryna Viazovska 8 维和 24 维球堆积结果的形式化证明。这份证明用 Lean 写成；Lean 是一种证明助手，即能自动检查证明每一步的软件。[^1, 3]Viazovska 于 2016 年证明了 8 维的结果，不久后又与合作者证明了 24 维的结果，这些工作为她赢得了 2022 年菲尔兹奖。[^2]据 IEEE Spectrum 2026 年 3 月 2 日报道，Math, Inc. 当天宣布了 24 维的成果，此前已于 2 月 23 日宣布 8 维的成果。[^3]

据洛桑联邦理工学院（EPFL）介绍，Formalising Sphere Packing in Lean 项目始于 2024 年，此前 Viazovska 在洛桑结识了数学家 Sidharth Hariharan。团队为 8 维证明撰写了详细的蓝图，即一份人类可读的路线图，标出证明的各个组成部分。随后，团队逐步把蓝图转写为 Lean。[^2, 3]

Math, Inc. 称，Gauss 随后用五天证明了 8 维情形所需的全部剩余结果。它还用两周时间完成了 24 维情形的形式化，输入只有原始论文，必要时检索文献。据该公司介绍，已发布的形式化成果约有 20 万行 Lean 代码；代码量最多时约达 50 万行，后经自动重构缩减。[^1]

EPFL 称 Gauss 发挥了决定性作用，并把这一作用描述为协助完成某些中间步骤。[^2]据 IEEE Spectrum 报道，Gauss 还发现并修正了已发表的 8 维论文中的一处笔误。该刊另外指出，在 24 维情形中，Gauss 没有人类撰写的蓝图可以依循。[^3]

:::analysis
这个项目在人与 AI 系统之间分工：人撰写蓝图，确定 8 维情形需要证明什么；AI 系统提供证明，交由 Lean 检查。Lean 接受了 AI 写出的证明，就意味着这些证明无需人类审稿人把关，前提是形式化命题（即用 Lean 写出的定理）与已发表的定理一致。对 24 维情形而言，这个前提更加关键，因为 Gauss 是在没有蓝图的情况下完成其形式化的。因此，独立审查其顶层命题会是下一步最有用的检查。
:::

:::checked
2026 年 10 月 20 日，我们阅读了 Math, Inc. 的文章、EPFL 2026 年 3 月 11 日发布的新闻和 IEEE Spectrum 2026 年 3 月 2 日的报道。Math, Inc. 的文章没有标注日期，因此我们依据 IEEE Spectrum 的报道确定其日期。我们没有编译这些 Lean 代码，也没有把其中的命题与已发表的定理比对。上述来源都没有提到对 24 维命题的独立审查。EPFL 和 IEEE Spectrum 称 24 维部分超过 20 万行，而 Math, Inc. 给出的约 20 万行是整个已发布形式化成果的规模。
:::