# Progress in Formalizing Sphere Packing in Dimension 8

arXiv: https://arxiv.org/abs/2604.23468 · HTML: https://mlsanity.com/paper/2604.23468/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- Builds on 2 of its 14 references that are in the map.
- First posted on arXiv 25 Apr 2026.

## Builds on (most cited first, 2 of 2)

- [A formal proof of the Kepler conjecture](https://mlsanity.com/paper/1501.02155/) (2015)
- [Mathematicians in the age of AI](https://mlsanity.com/paper/2603.03684/) (2026)

## Built on by (most cited first, 9 of 9)

- [Advancing Mathematics Research with AI-Driven Formal Proof Search](https://mlsanity.com/paper/2605.22763/) (2026)
- [AI co-mathematician: Accelerating mathematicians with agentic AI](https://mlsanity.com/paper/2605.06651/) (2026)
- [LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization](https://mlsanity.com/paper/2606.05400/) (2026)
- [Formalizing Mathematics at Scale](https://mlsanity.com/paper/2605.29955/) (2026)
- [Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge](https://mlsanity.com/paper/2606.11430/) (2026)
- [Explanations, Prompts, and Formalizations: Arguments for New Norms in LLM-Enabled Mathematical Research](https://mlsanity.com/paper/2608.29401/) (2026)
- [Math for AI safety: an invitation for mathematicians](https://mlsanity.com/paper/2609.15289/) (2026)
- [Choir: An Open Protocol for Distributed Multi-Agent Autoformalization](https://mlsanity.com/paper/2609.31903/) (2026)
- [The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization](https://mlsanity.com/paper/2610.14059/) (2026)

## Abstract (arXiv)

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.