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 optimalit