Progress in Formalizing Sphere Packing in Dimension 8
International Congress on Mathematical Software (ICMS) · Waterloo (ON), Canada · 23 July 2026
Links to website and paper
This talk is about the ongoing effort to formalise the solution the sphere packing problem in dimension 8. We discuss our progress this far, describe key design choices, reflect on significant milestones, and outline key objectives and challenges that remain. Based on joint work with Christopher Birkbeck, Seewoo Lee, Gareth Ma, Bhavik Mehta, Auguste Poiroux and Maryna Viazovska.