Back HomeUsing Gauss, we have helped formally verify the sphere packing problem in dimensions 8 and 24 — certifying that the E8 lattice and the Leech lattice achieve the densest possible arrangements of non-overlapping spheres in their respective dimensions.These results, originally proved by Maryna Viazovska and collaborators, earned Viazovska the Fields Medal at the 2022 International Congress of Mathematicians. This is the only formalization of a Fields Medal-winning result from this century ...