Sphere Packing in 8 & 24 Dims
Maryna Viazovska proved in 2016 that the E8 and Leech lattices pack equal spheres as densely as possible in 8 and 24 dimensions; Fields Medal 2022.
Open in the interactive tree →The sphere-packing question asks how densely identical spheres can fill space. In March 2016 Viazovska, then a postdoctoral researcher in Berlin, proved in a 23-page paper that the E8 lattice is the densest packing in eight dimensions, and a week later she and Henry Cohn with colleagues did the same for the Leech lattice in 24 dimensions. She received the Fields Medal on 5 July 2022 for this work. In March 2026 EPFL reported that both proofs had been formalised in the Lean proof assistant with help from an AI system (Gauss, by Math, Inc.), the dimension-24 case needing over 200,000 lines of code.
Prerequisites
Unlocks
- Formal Proofs (Lean, Rocq)2005-2026Both sphere-packing proofs were formalised in Lean with AI help in March 2026