Formalising 8-Dimensional Sphere Packing in Lean
(Joint talk with Chris Birkbeck and Seewoo Lee) · Lean Together 2026 · Online · 21 January 2026
Links to website and recording
In this talk, we discussed the ongoing effort to formalise Maryna Viazovska's Fields medal work on Sphere Packings in \(8\) dimensions. We recapped the main achievements thus far and the problems that still remained.