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.

## 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.