Formalising Sphere Packing in Lean

In 2022, Maryna Viazovska was awarded the Fields Medal for solving the sphere packing problem in dimension \(8\). This project formalises this result in the Lean Theorem Prover following her original paper and followup calculations by Lee. It is an online, open-source collaboration currently being led by Christopher Birkbeck, Sidharth Hariharan, Bhavik Mehta and Seewoo Lee. If you’d like to contribute, you may find the following links useful!

• Zulip chat for coordination
• Blueprint
• Blueprint as pdf
• Dependency graph
• Doc pages for this repository
• Project dashboard
• Viazovska’s original paper

Contributing

1. Make sure you have installed Lean.
2. Download the repository using git clone https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean.git.
3. Run lake exe cache get! to download built dependencies (this speeds up the build process).
4. Run lake build to build all files in this repository.
5. Read the CONTRIBUTING.md file in the repository for more information on how to contribute.

For more on getting started with Lean, visit the course repository for MATH60040/70040, Formalising Mathematics, taught by Bhavik Mehta at Imperial College London in Spring 2025.