Large-Scale Formalisation: A Student's Perspective
AI and Mathematics: Formalization, Theorem Proving, and Reasoning · Korea Institute for Advanced Study, Seoul, South Korea · 13 July 2026
Link to website
In March 2024, when I was a third-year undergraduate exchange student in Switzerland, I embarked on a collaboration with Maryna Viazovska to formalise her seminal solution to the sphere packing problem in dimension 8. In this talk, I will reflect on the process of learning through formalisation, drawing on examples from my own work and beyond. I will furthermore describe the many milestones we have achieved over the course of the project, challenges unique to the formal medium, and objectives that remain. The sphere packing project is joint work with Christopher Birkbeck, Seewoo Lee, Gareth Ma, Bhavik Mehta, Maryna Viazovska, and community contributors.