Viazovska's 2016 proof of optimal sphere packing in dimension 8 uses modular forms to construct a magic function satisfying Cohn-Elkies optimality conditions. Formalizing this proof in a theorem prover had not been completed prior to 2026.

The Sphere Packing project, launched in March 2024 by Hariharan and Viazovska, formalizes Viazovska's solution in the Lean theorem prover. Human formalizers built the initial blueprint and Lean development (~20,000 lines). In the final stages, Math, Inc.'s autoformalization model 'Gauss' completed a sorry-free formalization of the main theorem in five days, expanding the development to ~80,000 lines. A subsequent compression and refactoring pass reduced it to 60,000 lines. The paper discusses techniques used and the human-AI collaboration.

The result was formally verified in February 2026 with a sorry-free development of approximately 60,000 lines of Lean 4. The autoformalization model completed the bulk of the remaining formalization in five days, taking the project from 20,000 to 80,000 lines before compression.