Projects: Sphere Packing

Stream: ItaLean 2025

[Pietro Monticone]

This thread is dedicated to the Sphere Packing project:

• Repository: https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean
• Informal & Formal Manager: @Sidharth Hariharan

[Sidharth Hariharan]

Useful links:

1. Repository
2. My thesis

First objective: Proposition 4.4.6 using preceding lemmas in Section 4.4.1. We will state (but sorry out) Lemma 4.2.3, a direct dependency of the lemmas preceding Proposition 4.4.6.

[Sidharth Hariharan]

Draft PR: spherepacking#229

[Tito Sacchi]

I fixed some issues with the definitions we wrote today and started writing a proof of the first integral identity. I pushed the code to my fork, any advice is welcome! We can look at the code together tomorrow.

[Sidharth Hariharan]

General resources

• Project website
• Blueprint
• GitHub Repository
• GitHub Projects Dashboard
• Project Zulip channel (on the Leanprover Zulip)
• Viazovska's talk at Big Proof (where our repository was opened up for public contributions)
• My Master's thesis (a version that outlines our strategy for formalising the construction of the magic function)

[Tito Sacchi]

image.png
Moving forward with Cauchy-Goursat :+1:
It is quite painful to prove identities with I_2 and I_4 because your definitions use parametrizations such as z_2', z_4', but our formalization of Cauchy-Goursat uses interval integrals directly. We basically need another change of variables.

[Michael Rothgang]

We talked about this in person: feel free to share if what we discussed (providing a specialised version of change of variables as an auxiliary lemma, for now) helps.

[Tito Sacchi]

Thanks! Currently working on rewriting the integrals using some identities available elsewhere. I'll prove a general lemma for simple linear changes of variables next.

[Tito Sacchi]

lemma const_add_variable_change (x₁ x₂ x₁' : ℝ) :
  ∫ t in x₁..x₂, f t =
  ∫ t in x₁'..(x₁' + (x₂ - x₁)), f (t - (x₁' - x₁)) := sorry

This should do the job and should be provable fairly easily using the standard Mathlib API.