Abstract
We prove that the Leech lattice is the unique densest lattice in $\mathbb{R}^{24}$. The proof combines human reasoning with computer verification of the properties of certain explicit polynomials. We furthermore prove that no sphere packing in $\mathbb{R}^{24}$ can exceed the Leech lattice’s density by a factor of more than $1+1.65\cdot 10^{-30}$, and we give a new proof that $E_8$ is the unique densest lattice in $\mathbb{R}^8$.