Issues

• Prove ineqA and ineqB

  thefundamentaltheor3m/Sphere-Packing-Lean#479 · Filter by author seewoo5 opened on Sep 9, 2026
  2

  

• Poisson summation formula

  task
  thefundamentaltheor3m/Sphere-Packing-Lean#471 · Filter by author thefundamentaltheor3m opened on Sep 1, 2026
  3

  

• Update derivative and Serre derivative with upstreamed notation

  thefundamentaltheor3m/Sphere-Packing-Lean#459 · Filter by author seewoo5 opened on Aug 17, 2026
  

• Updates available but manual intervention required

  auto-update-lean-fail
  thefundamentaltheor3m/Sphere-Packing-Lean#455 · Filter by author github-actions opened on Jul 29, 2026

• Informalizing Poisson summation

  thefundamentaltheor3m/Sphere-Packing-Lean#412 · Filter by author viazovska opened on Apr 28, 2026

• Systematise bounding

  thefundamentaltheor3m/Sphere-Packing-Lean#404 · Filter by author thefundamentaltheor3m opened on Apr 21, 2026

• Adapt Double Zeroes proof (the Cameron-Claude-Tito proof) to $b$

  task
  thefundamentaltheor3m/Sphere-Packing-Lean#403 · Filter by author thefundamentaltheor3m opened on Apr 21, 2026

• Double Zeroes PR Stack

  thefundamentaltheor3m/Sphere-Packing-Lean#402 · Filter by author thefundamentaltheor3m opened on Apr 21, 2026

• Schwartzness: Adapting the definitions of the functions (for $a$ and $b$) to use a bump function so we can compose with norm squared

  task
  thefundamentaltheor3m/Sphere-Packing-Lean#401 · Filter by author thefundamentaltheor3m opened on Apr 21, 2026
  2

  

• null-measurable set

  thefundamentaltheor3m/Sphere-Packing-Lean#400 · Filter by author viazovska opened on Apr 20, 2026

• Priority List

  thefundamentaltheor3m/Sphere-Packing-Lean#397 · Filter by author thefundamentaltheor3m opened on Apr 15, 2026

• Very simple lemma

  thefundamentaltheor3m/Sphere-Packing-Lean#395 · Filter by author viazovska opened on Apr 15, 2026
  3

• Things to be upstreamed

  thefundamentaltheor3m/Sphere-Packing-Lean#368 · Filter by author seewoo5 opened on Mar 18, 2026

• [blueprint] SpherePacking remark prevents depgraph nodes from turning dark green

  thefundamentaltheor3m/Sphere-Packing-Lean#294 · Filter by author dwrensha opened on Jan 19, 2026

• False example in SpherePacking/MagicFunction/PolyFourierCoeffBound.lean

  thefundamentaltheor3m/Sphere-Packing-Lean#223 · Filter by author lawrence-harmonic opened on Dec 3, 2025

• Upstream ENat.lean and ENCard.lean

  thefundamentaltheor3m/Sphere-Packing-Lean#178 · Filter by author b-mehta opened on Nov 10, 2025
  1

• Split up calc_steps

  task
  thefundamentaltheor3m/Sphere-Packing-Lean#104 · Filter by author thefundamentaltheor3m opened on Jun 15, 2025
  1

  

• Proving that the periodic sphere packing constant equals the sphere packing constant in all dimensions

  task
  thefundamentaltheor3m/Sphere-Packing-Lean#80 · Filter by author thefundamentaltheor3m opened on Jun 13, 2025
  9

  

• Filling sorrys in Cohn-Elkies

  task
  thefundamentaltheor3m/Sphere-Packing-Lean#79 · Filter by author thefundamentaltheor3m opened on Jun 13, 2025
  2

• Proving the double zeroes property for $a$

  task
  thefundamentaltheor3m/Sphere-Packing-Lean#77 · Filter by author thefundamentaltheor3m opened on Jun 13, 2025
  2

  

• State the double zeroes integrals and prove basic properties

  task
  thefundamentaltheor3m/Sphere-Packing-Lean#76 · Filter by author thefundamentaltheor3m opened on Jun 13, 2025
  2

  

• State and prove that the Iⱼ and Jⱼ are integrable over ℝ⁸

  task
  thefundamentaltheor3m/Sphere-Packing-Lean#75 · Filter by author thefundamentaltheor3m opened on Jun 13, 2025
  2

  

• Bounding J₁,...,J₆

  task
  thefundamentaltheor3m/Sphere-Packing-Lean#74 · Filter by author thefundamentaltheor3m opened on Jun 13, 2025
  2