Website

The sphere packing problem. Abstract. In the first lecture, I will discuss the history of the sphere packing problem, the known upper and lower bounds, and its solution in dimensions 8 and 24. I will introduce the magic functions and explain how they are constructed.

Fourier interpolation formulas. Abstract. In the second lecture, I will discuss Fourier interpolation formulas and their connection with the magic functions. As an application, I will show how such an interpolation formula leads to the universal optimality of the E8 and Leech lattices.

Formalizing sphere packing. Abstract. In the final lecture, I will describe the path toward formalizing the sphere packing problem in dimensions 8 and 24. I will discuss the main milestones reached so far, the role of AI, and the challenges posed by large-scale formalization projects.