The Road to Formalising 8-Dimensional Sphere Packing in Lean
Formalisation of Mathematics with Interactive Theorem Provers · University of Cambridge, Cambridge, United Kingdom · 9 October 2025
Links to website and recording
In this talk, I presented my ongoing work on formalising the packing of 8-dimensional spheres in the Lean theorem prover. I discussed progress and challenges and outlined avenues for community contributions.