Completing the formal proof of higher-dimensional sphere packing

Using 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 (GitHub).

The Problem

How densely can identical spheres be packed in n-dimensional space? In one dimension, the problem is trivial, and in two dimensions, elementary proofs have existed for decades. In three dimensions, a solution was conjectured by Kepler in 1611, but it was not proved until Thomas Hales settled it in 1998, in a heavily computer-assisted proof that subsequently took over a decade to formally verify.

The problem was not solved in any other dimensions until Viazovska discovered an astonishing connection to the theory of modular forms and solved the problem in dimension 8. Within days, Cohn, Kumar, Miller, Radchenko and Viazovska used similar techniques to solve the problem in dimension 24. To this day, the problem remains unsolved in all other dimensions.

Viazovska's remarkable construction, famously described by Peter Sarnak as "stunningly simple, as all great things are," earned her the Fields Medal, widely considered the "Nobel Prize of mathematics." She has since proved more results about the theory she developed, such as universal optimality. The solutions in dimensions 8 and 24 rely on a sophisticated interplay between discrete geometry, harmonic analysis, and number theory, making it one of the most impressive results in 21st-century mathematics.

The Formalization Process

In 2024, the project to formalize the 8-dimensional solution was launched jointly by Sidharth Hariharan and Maryna Viazovska. Together with Chris Birkbeck, Seewoo Lee, Gareth Ma and Bhavik Mehta, they wrote a detailed blueprint and developed an extensive codebase consisting of new definitions and theorems about sphere packings, lattices, and (quasi)modular forms that were absent from Mathlib.

We first began collaborating with the Sphere Packing maintainers in November 2025. After successfully proving several facts about modular forms, radial Schwartz functions, and basic sphere packing theory using a previous version of Gauss, we set our sights on a more ambitious goal: completing the remainder of the project.

In just 5 days, Gauss automatically proved all remaining results needed to verify the result in 8 dimensions. The Sphere Packing team estimated that the 8-dimensional case alone would have taken six more months of work with existing tools. In two weeks, Gauss then autoformalized the 24-dimensional case using only the original paper as input, performing autonomous literature searches when needed. This brought the total sphere packing formalization from 70k to ~200k lines.

Along the way, Gauss autonomously proved numerous important facts about modular forms, discrete geometry, contour integration and Fourier analysis. Gauss's contribution to this project has accelerated the verification of this extraordinary result at an unprecedented pace. This is a historic achievement in autoformalization.

Scale

3,500 lines (de Bruijn, June 2025)
25,000 lines (Strong Prime Number Theorem, September 2025)
~200,000 lines (Sphere Packing formalization, February 2026)

The largest single-purpose formalization projects human teams have taken on — efforts that can define careers and take a decade or longer — rarely exceed around 500,000 lines. Mathlib, the cumulative work of over 600 contributors since 2017, stands at approximately 2 million lines. Using Gauss, a three-week effort now reaches a scale that, until very recently, required years.

Looking Ahead

Formalizing mathematics will accelerate research by making the full landscape of known results searchable, composable, and machine-navigable. Formalizing results like 8- and 24-dimensional sphere packing deepens our understanding of the unity of mathematical knowledge by rigorously proving deep structural connections between areas of mathematics that can seem unrelated.

A formal proof that compiles without errors is not the end of the story. The harder and more consequential challenges lie in what comes next: organizing, integrating, and maintaining formal knowledge at a planetary scale. These are challenges that the world will confront over the coming years as an increasing number of proofs are produced by AI systems. The ability to integrate these proofs into an ever-expanding, intercompatible knowledge base will soon be a basic requirement for scale. We will continue to collaborate with the maintainers of the sphere packing project and other libraries of formal mathematics to ensure the code Gauss has produced remains usable and maintainable for posterity. As a first step in that direction, we used Gauss to automatically refactor, optimize, and improve the style of the formalization it produced, effectively decreasing its size from 500,000 lines at peak to the released version of ~200,000 lines.

Acknowledgements

We gratefully acknowledge the support of DARPA's expMath program. We are also grateful to all our collaborators from the Lean community, led by Chris Birkbeck, Sidharth Hariharan, Seewoo Lee, Bhavik Mehta and Maryna Viazovska, and acknowledge the invaluable support of Jeremy Avigad, Kevin Buzzard, David Loeffler, Gareth Ma, Pietro Monticone, the Mathlib maintainers and the Institute for Computer-Aided Reasoning in Mathematics.

You can register for early access to Gauss here. If you have an ambitious idea for autoformalization, we'd like to hear from you.

For press inquiries, contact contact@math.inc.

Math, Inc.