Sphere packing: the proof, the code, and the people

A packing is a set of non-overlapping balls of equal radius. Its density is the fraction of space they fill, measured in ever larger balls $B_R$:

In the plane the hexagonal packing is best, with density $\pi / \sqrt{12} \approx 0.9069$ (Thue; Fejes Tóth, 1940). In three dimensions the familiar stacking of oranges, with density $\pi / \sqrt{18} \approx 0.7405$, is optimal: that is the Kepler conjecture, proved by Hales (announced 1998, published 2005) and formally verified by the Flyspeck project in 2014. Before 2016, no other dimension was solved.

Cohn and Elkies (2003) turned packing into a question about a single function. Suppose $f: \mathbb{R}^n \to \mathbb{R}$ is a well-behaved function with Fourier transform $\hat f$ such that

Then every packing of $\mathbb{R}^n$ has density at most $\operatorname{vol}\big(B^n_{r/2}\big)$, the volume of a ball of radius $r/2$. For a lattice packing the proof is Poisson summation, $\sum_{v \in \Lambda} f(v) = \frac{1}{\operatorname{vol}(\mathbb{R}^n / \Lambda)} \sum_{w \in \Lambda^*} \hat f(w)$: the left side is at most $f(0)$ and the right side at least $\hat f(0) / \operatorname{vol}(\mathbb{R}^n / \Lambda)$.

In dimension $8$ the lattice $E_8$ has covolume $1$ and shortest vectors of length $\sqrt{2}$, so balls of radius $\sqrt{2}/2$ fit, and its density is

The bound matches exactly if a function with $r = \sqrt{2}$ exists, and then it must vanish at every length $\sqrt{2k}$ of a nonzero $E_8$ vector. Numerical evidence suggested it existed; Viazovska built it in 2016 from modular forms, whose symmetries under $\tau \mapsto -1/\tau$ are what make $f$ and $\hat f$ fit together. A week later, with Cohn, Kumar, Miller and Radchenko, she did the same for the Leech lattice in dimension $24$, with $r = 2$.

The proof combines Fourier analysis on $\mathbb{R}^n$ and Poisson summation, the theory of modular forms and their $q$-expansions, and explicit inequalities showing that $f \le 0$ and $\hat f \ge 0$ where required. Each of these needs a library: definitions, basic lemmas and their interfaces have to exist in Lean before the final argument can even be stated.