Sphere Packing in R^8

 Sphere Packing in Lean🔗

Compiled2026-08-09T18:32:35ZProjectbbeb73aMerge pull request #17 from ejgallego/chore/refresh-vbp-457b3f4Leanleanprover/lean4:v4.32.0VersoBlueprint7764b37Upstreambad3de9feat(ForMathlib/RadialSchwartz): the submodule of radial Schwartz functions (#444)Mathlibv4.32.0@81a5d257c8e4
Maryna ViazovskaSphere Packing in Lean collaborators

Contents

  1. 1. Overview
  2. 2. Sphere Packings
  3. 3. Density of Packings
  4. 4. The E8 Lattice
  5. 5. Fourier Analysis
  6. 6. Cohn-Elkies Bounds
  7. 7. Modular Forms
  8. 8. Fourier Eigenfunctions with Double Zeroes
  9. 9. Proof of the Optimal Function Inequalities
  10. Dependency Graph
  11. Blueprint Summary
  12. Blueprint Bibliography