用形式化证明验证8维球体堆积最优解，人类与AI协同完成。
Progress in Formalizing Sphere Packing in Dimension 8
- 借助模形式构造'魔法函数'，证明8维球体堆积最优。
- 2026年2月由Gauss模型完成最终形式化验证。
- 展示人类与AI在数学证明中的深度协作潜力。
2016年，Viazovska利用模形式构造出满足Cohn和Elkies于2003年提出的最优性条件的‘魔法’函数，从而解决了8维球体堆积问题。2024年3月，Hariharan与Viazovska启动项目，将该解法及相关数学事实在Lean定理证明器中进行形式化。2026年2月，项目取得重大进展：结果经形式化验证完成，最后阶段由Math, Inc.开发的自动形式化模型‘Gauss’实现。本文探讨达成这一里程碑所采用的技术，反思人类与Gauss之间的独特协作模式，并讨论尚未完成的项目目标。
原文摘要 · Abstract (English)
In 2016, Viazovska famously solved the sphere packing problem in dimension $8$, using modular forms to construct a 'magic' function satisfying optimality conditions determined by Cohn and Elkies in 2003. In March 2024, Hariharan and Viazovska launched a project to formalize this solution and related mathematical facts in the Lean Theorem Prover. A significant milestone was achieved in February 2026: the result was formally verified, with the final stages of the verification done by Math, Inc.'s autoformalization model 'Gauss'. We discuss the techniques used to achieve this milestone, reflect on the unique collaboration between humans and Gauss, and discuss project objectives that remain.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。