This project attempts to formalise some notions about Sphere Packing in Lean. Important links:

• Landing Page
• Zulip Chat
• GitHub Project Page
• Blueprint (web version)
• Dependency Graph (web version)
• Blueprint (PDF version)
• API Documentation

This project was kickstarted at EPFL by Maryna Viazovska and Sidharth Hariharan in March 2024. It is currently being maintained by Christopher Birkbeck, Sidharth Hariharan, Bhavik Mehta and Seewoo Lee. Contributions welcome: see below for more details.

Should you wish to make any contributions to the content of the project, please add them to a new branch and make a pull request. Your PR will need to satisfy certain status checks, be approved by a reviewer and have no conflicts with the base branch before it can be merged. Please read CONTRIBUTING.md for details.