Sphere Packing 项目复盘：Math Inc 的 Gauss 完成 8 维与 24 维球填充形式化

Lean 形式化项目 Sphere Packing Project 发布博客第一篇，讲述从 2023 年 Kevin Buzzard 在 EPFL 的讲座牵线、Sidharth Hariharan 与 Maryna Viazovska 合作，到 2025 年 6 月仓库公开、社区贡献与 packathon 协作的全过程。