The Road to Formalising 8-Dimensional Sphere Packing in Lean

Add to your list(s) Download to your calendar using vCal

• Sidharth Hariharan (Carnegie Mellon University)
• Thursday 09 October 2025, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

If you have a question about this talk, please contact Anand Rao Tadipatri.

In 2022, Maryna Viazovska was awarded the Fields Medal for an outstanding achievement: solving the sphere packing problem in dimension 8. The ingenuity of Viazovska’s solution stems from her combination of techniques from the apparently unrelated theories of radial Schwartz functions and modular forms to construct a so-called “magic function”, using which one can show that the density of the E₈ sphere packing is an upper-bound for all sphere packings in dimension 8.

Around 18 months ago, I embarked on a venture to really put the capabilities of Lean to test: I began a project to formalise Viazovska’s groundbreaking solution. Never before has work that is both as recent and as highly acclaimed as Viazovska’s been formalised, and if this project succeeds, it will be an important milestone for the formalisation movement.

This talk is based on joint (and ongoing) work by Birkbeck, Hariharan, Ma, Mehta, Lee, Viazovska, and open-source contributors.

=== Hybrid talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY.1

Meeting ID: 898 5609 1954 Passcode: ITPtalk

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• Martin's interesting talks
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk449

Note that ex-directory lists are not shown.