Sphere packing: the proof, the code, and the people
Gauss completes major formalization work built on a community project.
Maryna Viazovska · sphere-packing community · Math, Inc. / Gauss
Start with the question
The problem
How densely can identical non-overlapping balls fill space? Viazovska solved the eight-dimensional problem in 2016; with Cohn, Kumar, Miller, and Radchenko, she also settled dimension 24. Formalizing these proofs requires geometry, harmonic analysis, and modular forms.
01
Before the automated finish
The community project began in 2024. Its contributors built definitions, modular-form infrastructure, and a blueprint for the argument. Their own history describes contributions from many mathematicians and experiments with more than one AI tool. This groundwork is part of the achievement. [2]
02
What Gauss contributed
Math, Inc. reports that Gauss completed the remaining eight-dimensional work in five days and formalized the 24-dimensional case over two weeks. It released a roughly 200,000-line development. These are formalizations of known human theorems, rather than new discoveries of the optimal lattices. [1][3]
03
The project continues after compilation
The community describes reviewing the generated code and preparing it for integration. The project’s research paper treats the February milestone as one stage in a continuing collaboration. Maintainable definitions and reusable library results matter alongside the existence of a checked final theorem. [4][5]
Inspect the evidence
The Lean formalization
Released Lean artifact; community integration continues
Math, Inc.’s repository contains the 8- and 24-dimensional formalizations. The community project has its own maintenance and review process. A complete artifact in a company fork does not imply that all of its code has been merged into the community library.
Open the Lean project ↗Sources & further reading
Reviewed 9 Sept 2026. X permalinks were recovered from indexed posts and linked discussions; direct X pages were not consistently accessible. They document the conversation, not proof correctness.
- 1.
- 2.
- 3.
- 4.
- 5.
- 6.