The Curious Case of Sphere Packing in Lean
(Virtual talk) · Workshop affiliated to the 17th International Conference on Interactive Theorem Proving (ITP) and the Federated Logic Conferences (FLoC) · Lisbon, Portugal · 25 July 2026
Link to website
Reflections on what the sphere packing project has taught us about large collaborative formalisation — and about how humans and machines can prove theorems together.