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!

Milestone: A sorry-free Proof

On 23 February, 2026, the sphere packing team announced the existence of a sorry-free proof of the solution to the sphere packing problem in dimension $8$. Particularly notable is the role played by Gauss, an autoformalisation agent developed by Math, Inc. Working off of the sphere packing repository as it was in mid-January, Gauss autonomously formalised all remaining project goals to achieve a complete sorry-free proof of this extraordinary result. Gauss has also produced an autoformalisation of the closely related sphere packing problem in dimension $24$. See the official press release for more details about this historic accomplishment.

A sorry-free result is not the end of the story. The Gauss PR for dimension $8$ needs extensive modification, refactoring, golfing and reorganisation before it can be merged. We are already collaborating with Math Inc on this, but we cannot do this without broader community support! We need your help to get this code merged in a maintainable, reusable way!

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.

Prospective contributors are also invited to join the packathons that take place every Tuesday at 10:30 am Eastern Time (15:30 UTC). These are informal meetings where we discuss project progress and avenues to contribute. In light of the autoformalisation, we are using the packathons to work together on reviewing the Gauss code and getting it ready to merge.