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
This talk is about recent progress in the sphere packing project, with particular emphasis on the unique challenge of balancing progress towards finishing the project and cleaning up an AI-generated formal verification. We reflect on the successes and failures of this process and its implications for the future of AI-generated formal mathematics, particularly reflecting on what distinguishes a formal verification from a true formalisation.