Progress in Formalizing Sphere Packing in Dimension 8 事件

Progress in Formalizing Sphere Packing in Dimension 8 arXiv:2604.23468v3 Announce Type: replace-cross Abstract: 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