Sphere Packing in Lean

Christopher Birkbeck, Sidharth Hariharan, Seewoo Lee,
Gareth Ma, Bhavik Mehta and Maryna Viazovska

This blueprint consists of an adaptation of Maryna Viazovska’s Fields Medal-winning paper proving that no packing of unit balls in Euclidean space \(\mathbb {R}^8\) has density greater than that of the \(E_8\)-lattice packing. You can view the contents of the current version of this page in PDF form here.

This formalisation project was kickstarted at EPFL by Maryna Viazovska and Sidharth Hariharan, and the contents of this blueprint were originally written by Maryna Viazovska on the suggestion of Kevin Buzzard. It is being updated and restructured by those involved in the formalisation effort. We express our sincere gratitude to Jeremy Avigad, Kevin Buzzard, David Loeffler, Pietro Monticone, David Renshaw, Utensil Song, the Mathlib maintainers, the Institute for Computer-Aided Reasoning in Mathematics, and everyone in the Lean Community for their invaluable contributions and support.