开发 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]

来源

  1. Completing the formal proof of higher-dimensional sphere packingMath, Inc. · 2026年3月2日
  2. Prof. Viazovska's proofs of sphere packing formalized with AIEPFL · 2026年3月11日
  3. Watershed Moment for AI–Human Collaboration in MathIEEE Spectrum · 2026年3月2日

核查或更正本页

更正
提交更正请求 · 在 GitHub 编辑源文件 · 更正政策
验证记录

下方摘要可以说明你读到的文字是否与公开的源文件一致，但不能说明报道内容本身正确。这一摘要在构建时根据本页的 Markdown 源文件计算，并列入站点清单。

2d7473c70cf7c971f5f08eeafef2a2ace60f6abb3b94ef0dd2f983c52d6cd93c

查看源文件 · 清单