Announcements

Stream: Sphere packing in 8 dimensions

[Sidharth Hariharan]

Welcome to the sphere packing project! We're extremely pleased to be taking this project public, following Maryna Viazovska's talk at Big Proof 2025. This Zulip channel is where we will be coordinating the effort.

1. Who are "we"? We are extremely grateful to Maryna Viazovska for having initiated this project and helped write the blueprint. The Lean code is being maintained by @Chris Birkbeck, myself, @Seewoo Lee and @Bhavik Mehta.
2. What is the "effort"? We are attempting to formalise Maryna Viazovska's Fields Medal-winning solution to the sphere packing problem in dimension $8$.
3. How can you get involved? We have a blueprint, a repository, documentation, and a project dashboard. We also have a landing page with links to all of these pages.

We look forward to your contributions!

[Kim Morrison]

I've created a linkifier for you, at Pietro's request. spherepacking#102.

[Sidharth Hariharan]

Thank you, Kim and Pietro!

[Bhavik Mehta]

Nice idea! Thanks :D

[Sidharth Hariharan]

Hi everyone! @Kim Morrison has been kind enough to create a sphere packing label on Mathlib for any PRs related to this project. Thought I’d let everyone know!