Paper reports the February 2026 formal verification of Viazovska’s 2016 dimension-8 sphere packing proof in Lean, with final stages completed by Math, Inc.’s autoformalization model Gauss.
Key Takeaways
Viazovska’s 2016 proof used modular forms to construct a “magic” function meeting Cohn-Elkies 2003 optimality conditions; the Lean formalization targets that exact argument.
Hariharan and Viazovska launched the Lean formalization project in March 2024; milestone reached February 2026, roughly 23 months of work.
Math, Inc.’s model Gauss handled the final formalization stages, marking a concrete human-AI collaboration on a Fields Medal-level result.
The project follows the precedent of Hales, who formally verified his own computer-assisted Kepler conjecture proof; dimension-8 continues that lineage.
Related calculations by Lee and additional infrastructure were formalized alongside the main theorem, with stated remaining project objectives.
