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公司的自动形式化模型“高斯”完成。我们讨论了实现这一里程碑所使用的技术，反思了人类与高斯之间独特的合作，并探讨了仍需完成的项目目标。