The Road to Formalising 8-Dimensional Sphere Packing in Lean
Graduate Student and Postdoc Seminar · Carnegie Mellon University, Pittsburgh (PA), United States · 11 September 2025
Link to 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.