A Lean Formalisation of Sphere Packing in Dimension 8
Swiss Mathematical Society Spring Meeting: Formalisation and Proof Assistants · UniDistance Suisse, Brig (VS), Switzerland · 27 March 2026
Links to website and recording
Arguably one of the most important sphere packing talks past and future, this talk was the first since the Gauss autoformalisation. I discussed progress made so far, commented briefly on the Gauss code, emphasised that the project was not over, and reflected on the ramifications for the future of formalised mathematics.