Eliminating the reliance on computer calculations in the sphere packing problem in dimension 8

What is it about?

The sphere packing problem is the mathematical problem of determining the densest way to pack spheres of equal radius in space. The original problem concerning three-dimensional spheres was posed by Johannes Kepler in 1611 and stood open for close to 400 years before being resolved definitively by Thomas Hales in 1998; mathematicians continue to study the problem in higher dimensions. In 2017, Maryna Viazovska gave a remarkable solution to the sphere packing problem in dimension 8 when she proved that the optimal 8-dimensional sphere packing is the one associated with the E8 lattice. The current paper improves on one part of Viazovska's solution in which she relied on computer calculations to verify a pair of analytical inequalities her proof depended on. We give a short and human-readable proof of those inequalities, resulting in a more streamlined and conceptual argument.

Featured Image

Photo by Martin Martz on Unsplash

Photo by Martin Martz on Unsplash

Why is it important?

Many mathematical theorems over the last 50 years have been proved with the aid of large amounts of computer calculations, such that a human mathematician cannot hope to verify by hand each detail of the calculation in a reasonable amount of time. A famous example is the four color theorem — the statement that four colors suffice to color countries on a map in such a way that countries that share a border are not colored using the same color; all known proofs of this result require a computer to verify. Proofs that involve computer calculations, known as computer-assisted proofs, are accepted by mathematicians as formally correct, but from a conceptual point of view many mathematicians believe that a completely human-readable proof not relying on extensive calculations will always provide a higher level of insight and understanding into the underlying structure of a mathematical question. Thus, it is considered desirable to find human-readable proofs of important theorems. The current paper does this for the case of the solution to the sphere packing problem in dimension 8.