Gauss: complete formalization of E₈ optimality in ℝ⁸ by augustepoiroux · Pull Request #341 · thefundamentaltheor3m/Sphere-Packing-Lean

augustepoiroux · 2026-02-23T17:24:24Z

Summary

This PR completes the Lean formalization of the theorem that the optimal sphere packing in ℝ⁸ is the E₈ lattice packing.
The branch contains the final theorem together with all remaining dependencies, and is checked by the Lean kernel (sorry-free).

Context

The code in this branch was generated by Gauss (Math Inc’s autoformalization agent) starting from the existing Sphere Packing blueprint and Lean codebase, and then packaged into this PR for review.

Notable changes

Completes the remaining formalization steps needed for E₈ optimality in ℝ⁸
Project-wide cleanup / proof golf (including existing files)
Fixes a sign inconsistency in Prop. 7 (b(t)), with the downstream definition of g in Thm. 4 updated accordingly
Migrates to the new module system
Bumps Lean to v4.28.0

Review notes

We made a best effort to avoid overwriting parts of the codebase that changed independently on main. As such, some results may be duplicated.
~~The following blueprint-linked Lean statements were commented out in this branch: ModularForm.dimension_level_one, dim_gen_cong_levels, D_qexp_tsum_pnat,serre_D_two_H₃`~~ -> they have been added back in 38876bc#diff-ebf1c68f284079a6364607bb7113a4b517ffb358424f42f02a128c225340f25d

dwrensha · 2026-02-23T17:56:21Z

+              let A : SchwartzMap.dualLattice (d := d) P.lattice → ℂ :=
+                SpherePacking.CohnElkies.expSum P D
+              let r : SchwartzMap.dualLattice (d := d) P.lattice → ℝ := fun m =>
+                (𝓕 ⇑f (m : EuclideanSpace ℝ (Fin d))).re * (‖A m‖ ^ 2)
+              have hFourier :
+                  ∀ m : SchwartzMap.dualLattice (d := d) P.lattice,
+                    𝓕 f (m : EuclideanSpace ℝ (Fin d)) = (𝓕 ⇑f) (m : EuclideanSpace ℝ (Fin d)) := by
+                intro m
+                simpa using congrArg (fun g : EuclideanSpace ℝ (Fin d) → ℂ =>
+                  g (m : EuclideanSpace ℝ (Fin d))) (SchwartzMap.fourier_coe (f := f))
+              have hterm :
+                  ∀ m : SchwartzMap.dualLattice (d := d) P.lattice,
+                    ((𝓕 f m).re : ℂ) * A m * conj (A m) = (r m : ℂ) := by
+                intro m
+                have hFourierRe :
+                    (𝓕 f m).re = (𝓕 ⇑f (m : EuclideanSpace ℝ (Fin d))).re := by
+                  simpa using congrArg Complex.re (hFourier m)
+                calc
+                  ((𝓕 f m).re : ℂ) * A m * conj (A m)
+                      = ((𝓕 f m).re : ℂ) * (A m * conj (A m)) := by
+                        simp [mul_assoc]
+                  _ = ((𝓕 f m).re : ℂ) * (‖A m‖ ^ 2) := by
+                        simp [Complex.mul_conj']
+                  _ = ((𝓕 ⇑f (m : EuclideanSpace ℝ (Fin d))).re : ℂ) * (‖A m‖ ^ 2) := by
+                        simp [hFourierRe]
+                  _ = (r m : ℂ) := by
+                        simp [r]
+              have hsum :
+                  (∑' m : SchwartzMap.dualLattice (d := d) P.lattice,
+                      ((𝓕 f m).re : ℂ) * A m * conj (A m))
+                    =
+                    ∑' m : SchwartzMap.dualLattice (d := d) P.lattice, (r m : ℂ) := by
+                exact tsum_congr fun m => hterm m
+              have hsum' :
+                  (∑' m : SchwartzMap.dualLattice (d := d) P.lattice, (r m : ℂ))
+                    =
+                    ((∑' m : SchwartzMap.dualLattice (d := d) P.lattice, r m : ℝ) : ℂ) := by
+                exact
+                  (Complex.ofReal_tsum (L := .unconditional _)
+                      (fun m : SchwartzMap.dualLattice (d := d) P.lattice => r m)).symm
+              -- Turn the complex series into an `ofReal` series, then take real parts.
+              have hcalc :
+                  ((1 / ZLattice.covolume P.lattice volume) *
+                        ∑' m : SchwartzMap.dualLattice (d := d) P.lattice,
+                          ((𝓕 f m).re : ℂ) * A m * conj (A m)).re
+                      =
+                      (1 / ZLattice.covolume P.lattice volume) *
+                        ∑' m : SchwartzMap.dualLattice (d := d) P.lattice,
+                          (𝓕 ⇑f (m : EuclideanSpace ℝ (Fin d))).re * (‖A m‖ ^ 2) := by
+                calc
+                  ((1 / ZLattice.covolume P.lattice volume) *
+                          ∑' m : SchwartzMap.dualLattice (d := d) P.lattice,
+                            ((𝓕 f m).re : ℂ) * A m * conj (A m)).re
+                      =
+                      ((1 / ZLattice.covolume P.lattice volume : ℂ) *
+                          ∑' m : SchwartzMap.dualLattice (d := d) P.lattice, (r m : ℂ)).re := by
+                        simp [hsum]
+                  _ = (1 / ZLattice.covolume P.lattice volume) *
+                      ∑' m : SchwartzMap.dualLattice (d := d) P.lattice, r m := by
+                        rw [hsum']
+                        simp
+                  _ = (1 / ZLattice.covolume P.lattice volume) *
+                      ∑' m : SchwartzMap.dualLattice (d := d) P.lattice,
+                        (𝓕 ⇑f (m : EuclideanSpace ℝ (Fin d))).re * (‖A m‖ ^ 2) := by
+                        rfl
+              -- Unfold `A` and rewrite `‖A m‖` as `norm (∑' x, ...)` (definitional).
+              simpa [A, r] using hcalc


In #302 I added a shorter proof of this section:

Suggested change

let A : SchwartzMap.dualLattice (d := d) P.lattice → ℂ :=

SpherePacking.CohnElkies.expSum P D

let r : SchwartzMap.dualLattice (d := d) P.lattice → ℝ := fun m =>

(𝓕 ⇑f (m : EuclideanSpace ℝ (Fin d))).re * (‖A m‖ ^ 2)

have hFourier :

∀ m : SchwartzMap.dualLattice (d := d) P.lattice,

𝓕 f (m : EuclideanSpace ℝ (Fin d)) = (𝓕 ⇑f) (m : EuclideanSpace ℝ (Fin d)) := by

intro m

simpa using congrArg (fun g : EuclideanSpace ℝ (Fin d) → ℂ =>

g (m : EuclideanSpace ℝ (Fin d))) (SchwartzMap.fourier_coe (f := f))

have hterm :

∀ m : SchwartzMap.dualLattice (d := d) P.lattice,

((𝓕 f m).re : ℂ) * A m * conj (A m) = (r m : ℂ) := by

intro m

have hFourierRe :

(𝓕 f m).re = (𝓕 ⇑f (m : EuclideanSpace ℝ (Fin d))).re := by

simpa using congrArg Complex.re (hFourier m)

calc

((𝓕 f m).re : ℂ) * A m * conj (A m)

= ((𝓕 f m).re : ℂ) * (A m * conj (A m)) := by

simp [mul_assoc]

_ = ((𝓕 f m).re : ℂ) * (‖A m‖ ^ 2) := by

simp [Complex.mul_conj']

_ = ((𝓕 ⇑f (m : EuclideanSpace ℝ (Fin d))).re : ℂ) * (‖A m‖ ^ 2) := by

simp [hFourierRe]

_ = (r m : ℂ) := by

simp [r]

have hsum :

(∑' m : SchwartzMap.dualLattice (d := d) P.lattice,

((𝓕 f m).re : ℂ) * A m * conj (A m))

=

∑' m : SchwartzMap.dualLattice (d := d) P.lattice, (r m : ℂ) := by

exact tsum_congr fun m => hterm m

have hsum' :

(∑' m : SchwartzMap.dualLattice (d := d) P.lattice, (r m : ℂ))

=

((∑' m : SchwartzMap.dualLattice (d := d) P.lattice, r m : ℝ) : ℂ) := by

exact

(Complex.ofReal_tsum (L := .unconditional _)

(fun m : SchwartzMap.dualLattice (d := d) P.lattice => r m)).symm

-- Turn the complex series into an `ofReal` series, then take real parts.

have hcalc :

((1 / ZLattice.covolume P.lattice volume) *

∑' m : SchwartzMap.dualLattice (d := d) P.lattice,

((𝓕 f m).re : ℂ) * A m * conj (A m)).re

=

(1 / ZLattice.covolume P.lattice volume) *

∑' m : SchwartzMap.dualLattice (d := d) P.lattice,

(𝓕 ⇑f (m : EuclideanSpace ℝ (Fin d))).re * (‖A m‖ ^ 2) := by

calc

((1 / ZLattice.covolume P.lattice volume) *

∑' m : SchwartzMap.dualLattice (d := d) P.lattice,

((𝓕 f m).re : ℂ) * A m * conj (A m)).re

=

((1 / ZLattice.covolume P.lattice volume : ℂ) *

∑' m : SchwartzMap.dualLattice (d := d) P.lattice, (r m : ℂ)).re := by

simp [hsum]

_ = (1 / ZLattice.covolume P.lattice volume) *

∑' m : SchwartzMap.dualLattice (d := d) P.lattice, r m := by

rw [hsum']

simp

_ = (1 / ZLattice.covolume P.lattice volume) *

∑' m : SchwartzMap.dualLattice (d := d) P.lattice,

(𝓕 ⇑f (m : EuclideanSpace ℝ (Fin d))).re * (‖A m‖ ^ 2) := by

rfl

-- Unfold `A` and rewrite `‖A m‖` as `norm (∑' x, ...)` (definitional).

simpa [A, r] using hcalc

rw [← ofReal_re (1 / ZLattice.covolume P.lattice volume *

∑' (m : ↥(LinearMap.BilinForm.dualSubmodule (innerₗ _) P.lattice)),

(𝓕 ⇑f ↑m).re * norm (∑' (x : ↑(P.centers ∩ D)),

cexp (2 * ↑π * I * ↑⟪(x : EuclideanSpace ℝ (Fin d)), ↑m⟫_[ℝ])) ^ 2)]

congr 1

push_cast

congr! 3 with m

rw [mul_assoc]

apply congrArg _ _

rw [mul_conj, Complex.normSq_eq_norm_sq]

norm_cast

Added back your proof in a new commit: 38876bc#diff-ebf1c68f284079a6364607bb7113a4b517ffb358424f42f02a128c225340f25d

dwrensha · 2026-02-23T18:01:21Z

-            rw [← ofReal_re (1 / ZLattice.covolume P.lattice volume *
-                ∑' (m : ↥(LinearMap.BilinForm.dualSubmodule (innerₗ _) P.lattice)),
-                 (𝓕 ⇑f ↑m).re * norm (∑' (x : ↑(P.centers ∩ D)),
-                 cexp (2 * ↑π * I * ↑⟪(x : EuclideanSpace ℝ (Fin d)), ↑m⟫_[ℝ])) ^ 2)]
-            congr 1
-            push_cast
-            congr! 3 with m
-            rw [mul_assoc]
-            apply congrArg _ _
-            rw [mul_conj, Complex.normSq_eq_norm_sq]
-            norm_cast


See my comment below. You deleted this proof and added a much longer proof of the same thing.

Thank you, sorry about that. We tried our best to incorporate recent changes, but failed in some places. Feel free to push more changes where needed.

Added back your proof in a new commit: 38876bc#diff-ebf1c68f284079a6364607bb7113a4b517ffb358424f42f02a128c225340f25d

b-mehta · 2026-02-23T18:15:16Z

+  toEquiv :=
+    { toFun := fun p => Fin.cons p.1 p.2
+      invFun := fun f => (f 0, fun i => f (Fin.succ i))
+      left_inv := by
+        rintro ⟨a, f⟩
+        ext <;> simp
+      right_inv := by
+        intro f
+        ext i
+        cases i using Fin.cases with
+        | zero => simp
+        | succ i => simp }
+  continuous_toFun := by
+    -- `Fin.cons` is continuous coordinatewise.
+    refine continuous_pi ?_
+    intro i
+    cases i using Fin.cases with
+    | zero =>
+        simpa using continuous_fst
+    | succ i =>
+        simpa using (continuous_apply i |>.comp continuous_snd)
+  continuous_invFun := by
+    refine (continuous_apply (0 : Fin n.succ)).prodMk ?_
+    refine continuous_pi ?_
+    intro i
+    simpa using (continuous_apply (Fin.succ i))


Suggested change

toEquiv :=

{ toFun := fun p => Fin.cons p.1 p.2

invFun := fun f => (f 0, fun i => f (Fin.succ i))

left_inv := by

rintro ⟨a, f⟩

ext <;> simp

right_inv := by

intro f

ext i

cases i using Fin.cases with

| zero => simp

| succ i => simp }

continuous_toFun := by

-- `Fin.cons` is continuous coordinatewise.

refine continuous_pi ?_

intro i

cases i using Fin.cases with

| zero =>

simpa using continuous_fst

| succ i =>

simpa using (continuous_apply i |>.comp continuous_snd)

continuous_invFun := by

refine (continuous_apply (0 : Fin n.succ)).prodMk ?_

refine continuous_pi ?_

intro i

simpa using (continuous_apply (Fin.succ i))

toEquiv := Fin.consEquiv (fun _ ↦ α)

continuous_toFun := by

simp only [Fin.consEquiv]

refine Continuous.finCons (by fun_prop) (by fun_prop)

continuous_invFun := by fun_prop

Added your change in 38876bc#diff-ebf1c68f284079a6364607bb7113a4b517ffb358424f42f02a128c225340f25d

Quite amazed by this golf by the way. I didn't check properly yesterday and thought it was a change that got overwritten by the merge. Next time I will use the "Commit suggestion" option instead.

dwrensha · 2026-02-23T21:52:33Z

Some improvements that tryAtEachStep found: math-inc#1

seewoo5 · 2026-02-23T22:44:20Z

It seems many of diffs include changing to the new module system - should we separate it as a new PR

seewoo5 · 2026-02-23T22:49:33Z


 /--
 If `F : ℍ → ℂ` is `O(exp(-c * im τ))` at `atImInfty` for some `c > 0`, then
 the restriction to the imaginary axis `t ↦ F(it)` is `O(exp(-c * t))` at `atTop`.
 -/
-lemma isBigO_resToImagAxis_of_isBigO_atImInfty {F : ℍ → ℂ} {c : ℝ} (_hc : 0 < c)
+lemma isBigO_resToImagAxis_of_isBigO_atImInfty {F : ℍ → ℂ} {c : ℝ}


We can make this (and other theorems use this) as a separate PR; it upgrades theorem by removing unnecessary assumption.

improvements found by tryAtEachStep

…ngly discarded during merge

dwrensha · 2026-02-24T14:10:08Z

Second round of improvements from tryAtEachStep: math-inc#2

more improvements found by tryAtEachStep

dwrensha · 2026-02-24T16:35:52Z

Some golfs with positivity: math-inc#4.

positivity improvements suggested by tryAtEachStep

seewoo5

For the part related to the modular form inequality (FG.lean, where Gauss splitted it into multiple files), it is essentially done once some open PRs are merged #248 #331 #307, so it is likely that the corresponding parts won't be needed (although there's a chance where Gauss's proof is better than current proofs). But something hasn't been formalized before is to connect the inequality FG_ineq_1 and FG_ineq_2 with the actual linear constraints of a and b that we definitely need - which I saw somewhere but cannot find it now (it was something like A_ineq or B_ienq).

seewoo5 · 2026-02-25T01:22:01Z

+    ResToImagAxis.Real.sub (ResToImagAxis.Real.mul hDFreal hGreal)
+      (ResToImagAxis.Real.mul hFreal hDGreal)
+
+private lemma L₁₀_over_tendsto_atImInfty :


Just as a note, this lemma (or whole file) won't be needed. This follows argument in v1 or v2 of my paper (2024 July), where the revised v3 (2025 August) uses new argument that avoids computation of $q$-expansion of $\mathcal{L}_{1,0}$. The new argument is already formalized as D_F_div_F_tendsto in #270 and D_G_div_G_tendsto in #239.

seewoo5 · 2026-02-25T01:25:13Z

@@ -1,74 +1,86 @@
-import Mathlib.Analysis.Normed.Group.Tannery


Large amount of this file are upstreamed and probably removed after bump #332

dwrensha · 2026-02-25T05:04:04Z

Even more from tryAtEachStep: math-inc#5

more improvements found by tryAtEachStep

Add improvements found by autoGolf

Auto golf 2

…343) `im_pnat_div_pos` was added upstream in leanprover-community/mathlib4@f160a5e. This change reduces the diff in #341. Gauss made the same change: https://github.com/math-inc/Sphere-Packing-Lean/blob/a6042330f897685ee6cd6d7a01e36e2460d60b18/SpherePacking/ModularForms/upperhalfplane.lean#L9

…print (#359) #239 proved `FmodG_strictAntiOn` in `FG.lean` and updated the blueprint to refer to it instead of `FmodG_antitone`. Concurrently, the gauss PR #341 split `FG.lean` into `FG/Basic.lean`, `FG/Inequalities.lean`, etc. That change was rebased in the `gauss2` branch, clobbering some of the work from #239. See [this bit of zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/509682-Sphere-packing-in-8-dimensions/topic/Gauss.20Rebase.20effort/near/578655616). One of the things that was clobbered was `FmodG_strictAntiOn`, which in the Gauss version is proved somewhat differently and has a different name `FmodG_strictAnti`. The present PR is a minimal change to get `leanblueprint all` working again. It renames gauss's `FmodG_strictAnti` to `FmodG_strictAntiOn`, to match the version from #239. It's possible that we might want to pull in other clobbered code from #239, but that can happen in a later PR.

Full formalization

d25e859

b-mehta reviewed Feb 23, 2026

View reviewed changes

Comment thread SpherePacking/ForMathlib/Intervals.lean Outdated

dwrensha reviewed Feb 23, 2026

View reviewed changes

b-mehta reviewed Feb 23, 2026

View reviewed changes

augustepoiroux and others added 2 commits February 23, 2026 19:46

Add back corollary results + few bad merge conflict resolutions

38876bc

improvements found by tryAtEachStep

9d272f0

seewoo5 reviewed Feb 23, 2026

View reviewed changes

augustepoiroux and others added 3 commits February 24, 2026 09:50

Merge pull request #1 from dwrensha/pr341-tryAtEachStep

92862ff

improvements found by tryAtEachStep

Add back some corollary results + proofs golfed by Gauss that got wro…

b6b9dff

…ngly discarded during merge

more improvements found by tryAtEachStep

a1e0153

augustepoiroux and others added 2 commits February 24, 2026 15:35

Merge pull request #2 from dwrensha/pr341-tryAtEachStep-2

797bf3c

more improvements found by tryAtEachStep

positivity improvements suggested by tryAtEachStep

39ec25c

thefundamentaltheor3m marked this pull request as draft February 24, 2026 16:51

Merge pull request #4 from dwrensha/tryAtEachStep-positivity

eae56f8

positivity improvements suggested by tryAtEachStep

seewoo5 reviewed Feb 25, 2026

View reviewed changes

seewoo5 mentioned this pull request Feb 25, 2026

feat(ModularForms): prove corrected MLDE for F and G (with E₄ factor) #248

Merged

2 tasks

more golfs found by tryAtEachStep

b59b31f

augustepoiroux and others added 7 commits February 25, 2026 09:04

Merge pull request #5 from dwrensha/tryAtEachStep-more

8c1ab42

more improvements found by tryAtEachStep

Add improvements found by autoGolf + a few other golfs

5cbf8c4

Merge pull request #6 from math-inc/autoGolf-1

052fccb

Add improvements found by autoGolf

autoGolf + Gauss pass

e42c4a5

More golfing

190c43b

Revert a few bad changes

958c514

Few more golfs

85af201

Merge pull request #7 from math-inc/autoGolf-2

a604233

Auto golf 2

dwrensha mentioned this pull request Mar 3, 2026

chore: prove pnat_div_upper by direct application of im_pnat_div_pos #343

Merged

dwrensha mentioned this pull request Mar 4, 2026

feat: norm_numI improvements from Gauss #345

Open

arajasek mentioned this pull request Mar 4, 2026

Move to the module system #346

Closed

arajasek mentioned this pull request Mar 12, 2026

feat: Gauss formalization of E₈ optimality in ℝ⁸ (rebased) #356

Draft

dwrensha mentioned this pull request Mar 12, 2026

[gauss2] rename FmodG_strictAnti to FmodG_strictAntiOn, to match blueprint #359

Merged

		@@ -1,74 +1,86 @@
		import Mathlib.Analysis.Normed.Group.Tannery

Conversation

augustepoiroux commented Feb 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Context

Notable changes

Review notes

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dwrensha commented Feb 23, 2026

Uh oh!

seewoo5 commented Feb 23, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dwrensha commented Feb 24, 2026

Uh oh!

dwrensha commented Feb 24, 2026

Uh oh!

seewoo5 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dwrensha commented Feb 25, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

augustepoiroux commented Feb 23, 2026 •

edited

Loading