A Milestone in Formalization: The Sphere Packing Problem in Dimension 8

arXiv:2604.23468v1 Announce Type: 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...