Sphere Packing in Lean

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, namely, Sidharth Hariharan, Gareth Ma, Seewoo Lee and Christopher Birkbeck. Those involved in the effort express their sincere gratitude to Kevin Buzzard, Utensil Song, Bhavik Mehta, Patrick Massot, Yaël Dillies, and everyone in the Lean Community for their support.