Completing the formal proof of higher-dimensional sphere packing
3 days ago
- #Sphere Packing
- #Formal Verification
- #Fields Medal
- Gauss helped formally verify the sphere packing problem in dimensions 8 and 24, confirming the E8 and Leech lattices achieve the densest sphere arrangements.
- Maryna Viazovska's work on sphere packing in dimensions 8 and 24 earned her the 2022 Fields Medal, the only formalization of a Fields Medal-winning result this century.
- The sphere packing problem was unsolved in most dimensions until Viazovska's breakthrough, which connected the problem to modular forms theory.
- Viazovska's solution in dimensions 8 and 24 involves a sophisticated interplay between discrete geometry, harmonic analysis, and number theory.
- A project to formalize the 8-dimensional solution was launched in 2024, involving detailed blueprints and extensive codebase development.
- Gauss automated the proof process, completing the 8-dimensional case in 5 days and the 24-dimensional case in two weeks, significantly accelerating the verification.
- Gauss autonomously proved numerous facts about modular forms, discrete geometry, and Fourier analysis during the project.
- The formalization effort reached ~200k lines, a scale previously requiring years of human effort.
- Formalizing mathematics accelerates research by making results searchable and composable, deepening understanding of mathematical connections.
- Future challenges include organizing, integrating, and maintaining formal knowledge at a planetary scale as AI-produced proofs increase.
- Gauss was used to refactor and optimize the formalization, reducing its size from 500k to ~200k lines.
- The project acknowledges support from DARPA's expMath program and collaboration with the Lean community and other mathematicians.