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 | Kutubxona