Source-linked AI summary
Progress in Formalizing Sphere Packing in Dimension 8
Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, Maryna Viazovska
TL;DR
The paper addresses the formal verification of Viazovska’s dimension-8 sphere-packing solution and related mathematics. It develops Lean definitions, formalizes key analytic and modular-form components, and reports a complete proof of optimality for the E8 lattice packing, while identifying limitations in code quality and correspondence with the intended proof.
Problem
The project seeks to formalize Viazovska’s dimension-8 sphere-packing solution and related mathematical facts in Lean.
Source: §1 · pp. 1–2Method
The formalization defines sphere packings and density in Lean and develops the analytic, Fourier-transform, and modular-form machinery needed for the proof.
Source: §2.1 · p. 2, §2.2 · p. 5, §2.3 · p. 6Results
The human-and-Gauss collaboration produced a complete, correct proof that the optimal sphere packing in R^8 is the E8 lattice packing.
Source: §1 · p. 2Takeaways & Limitations
The milestone provides a formal proof artifact while illustrating that autoformalization must improve reusable code quality alongside proof completion.
Source: §1 · p. 2, §3 · p. 7The project formalizes a slightly modified blueprint argument, and the exact correspondence between Gauss’s code and the intended proof path remains under investigation.
Source: §4 · p. 8
Abstract
from arXiv · showhide
In 2016, Viazovska famously solved the sphere packing problem in dimension $8$, using modular forms to construct a 'magic' function satisfying optimality conditions determined by Cohn and Elkies in 2003. In March 2024, Hariharan and Viazovska launched a project to formalize this solution and related mathematical facts in the Lean Theorem Prover. A significant milestone was achieved in February 2026: the result was formally verified, with the final stages of the verification done by Math, Inc.'s autoformalization model 'Gauss'. We discuss the techniques used to achieve this milestone, reflect on the unique collaboration between humans and Gauss, and discuss project objectives that remain.
1 Introduction
The paper introduces a Lean formalization project for Viazovska’s dimension-8 sphere-packing solution, aiming to produce a readable, maintainable, reusable proof artifact. The project has reached a complete, correct proof that the optimal packing in R^8 is the E8 lattice packing.
- The sphere packing problem asks for the densest arrangement of non-overlapping n-spheres in R^n and is notoriously difficult in discrete geometry.Source: §1 · p. 1
- In March 2024, Hariharan and Viazovska began formalizing Viazovska’s dimension-8 solution and related calculations in Lean.The project also builds infrastructure for ongoing and future work in related areas.Source: §1 · p. 1
- The combined work of human formalizers and Gauss produced a complete, correct proof that the optimal sphere packing in R^8 is the E8 lattice packing.The stated milestone is intended to yield a readable, maintainable, and reusable proof artifact.Source: §1 · p. 2
2 The Mathematics behind the 8-Dimensional Sphere Packing Problem
The project formalizes the mathematics underlying Viazovska’s proof that the E8 lattice is optimal in R8, developing Lean definitions, modular-form theory, contour arguments, and metaprogramming infrastructure.
2.1 The Road to Stating the Main Theorem
- Lean represents sphere packings through centres, a positive separation, disjointness conditions, balls, finite densities, and the limsup density.Periodic packings add a lattice action, and the sphere packing constant is defined as the supremum of packing densities.Source: §2.1 · pp. 2–3
- The formalized main theorem states that the sphere packing constant in dimension 8 equals the density of the E8 packing.This formalizes Viazovska’s result that no sphere packing in R8 has greater density than the E8 packing [14].Source: §2.1 · p. 3
2.2 Constructing Viazovska’s Magic Function in Lean
- Viazovska’s magic function uses radial Schwartz Fourier eigenfunctions built from quasimodular forms to satisfy the Cohn-Elkies optimality conditions.Contour choices and deformation arguments yield Laplace-transform representations, while Fourier eigenfunction identities reduce the remaining conditions to inequalities on the positive imaginary axis [10].Source: §2.2 · pp. 4–5, §2.1 · p. 4
2.3 The Theory of (Quasi)Modular Forms
- The project formalized modular-form infrastructure including E2, the discriminant form, derivatives, dimension formulas, Ramanujan identities, and Jacobi-theta identities.These developments support identities and inequalities needed in the magic-function proof, although the dimension-formula proof required non-standard methods because mathlib lacked contour-integration machinery.Source: §2.3 · p. 6
2.4 Metaprogramming
- New metaprogramming tactics automate complex-number normalization and continuity-based limit proofs for expressions involving quasimodular forms.The tactics include norm_numI for complex arithmetic and tendsto_cont for limits of continuous expressions.Source: §2.4 · pp. 6–7
3 Autoformalization
Gauss completed a sorry-free formalization of the main theorem and several substantial supporting results, while the resulting code still requires extensive cleanup for reuse and maintainability.
Autoformalization
- Five days produced a sorry-free formalization of the main theorem, expanding the development from about 20,000 to 80,000 lines before later refactoring.A subsequent compression and refactoring pass reduced the development to 60,000 lines.Source: §3 · p. 7
- Gauss completed dimension 8 contour-deformation identities for the Fourier eigenfunction argument, including a wedge-set deformation based on the Poincaré lemma.Source: §3 · p. 7
- The generated code often introduced unbundled auxiliary definitions, duplicated results, and proofs ranging from hundreds of lines to trivial special cases, complicating maintenance and compilation.Human cleanup is targeting these extremes to bring the development toward mathlib standards.Source: §3 · p. 7
4 A Look to the Future
The project’s future work centers on reconciling verification with its original goals of understanding Viazovska’s result and building reusable infrastructure. Although the sorry-free proof is a major achievement, the formalization uses a modified argument and its correspondence to the intended proof remains under investigation.
4 A Look to the Future
- The project produced a sorry-free proof, but Gauss’s direct verification route did not completely comply with the project’s original objectives.Those objectives included revisiting and better understanding Viazovska’s results while building libraries and infrastructure for future work.Source: §4 · p. 8
- Technically, the development formalizes a slightly modified blueprint argument rather than Viazovska’s original argument in its entirety.The main difference highlighted is the use of Lee’s original proof [10] for the inequalities.Source: §4 · p. 8
- The exact correspondence between Gauss’s large codebase and the intended proof path remains under investigation, and some parts may still use new proofs.This leaves the project’s final proof structure open to further analysis and refinement.Source: §4 · p. 8
- The authors view the collaboration as a distinctive achievement while expecting future work to document its formal and informal lessons in greater technical detail.Gauss’s direct use of human-written Lean code and the blueprint underscores the importance of robust definitions, detailed proof strategies, and thoughtful design choices.Source: §4 · p. 8