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.

翻译：2016年，维亚佐夫斯卡利用模形式构造了满足科恩与埃尔基斯于2003年确定的最优性条件的"魔法"函数，从而著名地解决了八维球堆积问题。2024年3月，哈里哈兰与维亚佐夫斯卡启动了一项在Lean定理证明器中形式化该解法及相关数学事实的项目。2026年2月取得重要里程碑：该结果通过形式化验证，其中最终阶段由Math公司的自动形式化模型"Gauss"完成。本文讨论了实现该里程碑所采用的技术，反思了人类与Gauss之间独特的协作模式，并阐述了尚待完成的项目目标。