Sphere Packing in Lean

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.

Contributing to the Project

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.

Acknowledgements

We are grateful to all contributors for their effort. We would also like to thank the Mathlib maintainers and the Lean community for their support. We are indebted to the Institute for Computer-Aided Reasoning in Mathematics for their help on matters of AI policy. Finally, we would like to thank G-Research for their generosity in partially supporting this research.