A Milestone in Formalization: The Sphere Packing Problem in Dimension 8 (Paper)