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