A Milestone in Formalization: The Sphere Packing Problem in Dimension 8. - Sidharth Hariharan; Christopher Birkbeck; Seewoo Lee; Ho Kiu Gareth Ma; Bhavik Mehta; Auguste Poiroux; Maryna Viazovska (CoRR, 2026)