Discussion for Autoformalization

Stream: Sphere packing in 8 dimensions

[Sidharth Hariharan]

Discussion thread for #announce > Sphere Packing Milestone

[Thomas Browning]

What ended up happening with the annoyingly shaped contour?

[Thomas Browning]

(My vague understanding is that the annoying contour was required for perm_I₁_I₂ and perm_J₁_J₂ in MagicFunction/a/Eigenfunction.lean and MagicFunction/b/Eigenfunction.lean respectively, but these files appear to have been deleted in the big PR).

[Thomas Browning]

(I guess it looks like these files were replaced by whole folders, which makes sense, but I'd still be curious to know how the autoformalization handled this difficulty).

[Bhavik Mehta]

For ease of search, the second one is now proved here: https://github.com/math-inc/Sphere-Packing-Lean/blob/d25e859461f8336daef05a40de36b51e11b621a9/SpherePacking/MagicFunction/b/Eigenfunction/FourierPermutations.lean#L38 with the important consequence in eig_b below.

[Kevin Buzzard]

That linksused to link to the PR in general: do you know which file it's in?

[Kevin Buzzard]

(Bhavik updated the link and answered my question)

[Bhavik Mehta]

Oops, it was meant to be a specific link - have edited.

[Anand Rao Tadipatri]

That's very interesting news! What was the timescale of the autoformalization, and by what factor was the task parallelized?

[Eric Wieser]

Aside from all the amazing prework by the human contributors of the sphere packing project, can you comment @Auguste Poiroux on the amount of human involvement in preparing thefundamentaltheor3m/Sphere-Packing-Lean#341? In particular:

• Did a human ask for or perform the upgrade to Lean 4.28.0?
• Did a human ask for or perform the module-ization of the source files?
• Was a human involved in writing the corrections to the norm_numI tactic?
• Did a human adjust the blueprint?

[Chris Birkbeck]

Just to note that in earlier versions there were also other things proved by Gauss that weren't strictly needed for the main result, but we had left in the blueprint as nice corollaries. For example, there was a proof of finite dimensionality for the spaces of modular forms for finite index levels (using the dimension result we proved in level one) which is a neat result we eventually want in mathlib.

[Auguste Poiroux]

What was the timescale of the autoformalization, and by what factor was the task parallelized?

It took 5 days for Gauss to get to a sorry-free proof.

• Did a human ask for or perform the upgrade to Lean 4.28.0?
• Did a human ask for or perform the module-ization of the source files?
• Was a human involved in writing the corrections to the norm_numI tactic?
• Did a human adjust the blueprint?

A human asked for the upgrade to Lean 4.28.0, modularization, and corrections to the norm_numI. No further hints on how to achieve that have been provided to Gauss. In comparison to the Strong PNT formalization, we did not adjust the blueprint, and we did not provide any mathematical hints.

[Auguste Poiroux]

Chris Birkbeck said:

Just to note that in earlier versions there were also other things proved by Gauss that weren't strictly needed for the main result, but we had left in the blueprint as nice corollaries. For example, there was a proof of finite dimensionality for the spaces of modular forms for finite index levels (using the dimension result we proved in level one) which is a neat result we eventually want in mathlib.

Yes indeed, it has been removed after the golf pass. We can add it back.

[Chris Birkbeck]

That would be great, thanks!

[Auguste Poiroux]

@Chris Birkbeck corollary results are back in the PR

[Eric Wieser]

Another question about human involvement; did humans resolve the merge conflicts with the latest version, or was this also performed by Gauss?

[Auguste Poiroux]

No this part was on me, so my fault for the bad merge conflict resolutions

[Eric Wieser]

Could you share a git history that indicates the actual version of the repo that gauss started with, and a separate commit for your conflict resolution?

[Auguste Poiroux]

Gauss started from this commit: https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean/commit/01a8d5b7acedb56523d0aac7de353888c7b459e9 but I won't be able to share anything related to git history beyond that.

[Eric Wieser]

What I was suggesting was creating an artificial git history consisting of that commit, with all the gauss changes applied on top of it as a single commit, then a real merge commit for your conflict resolution. Indeed I don't expect you to want to share any intermediate history produced by Gauss itself at this time!

[David Renshaw]

One of the things I really enjoyed about the AlphaZero news from few years back was the expert analysis of AlphaZero's chess games, for example:

• this book
• this youtube series
  

As the Sphere Packing project enters its next phase, I hope maybe its leaders can find inspiration in these works. In addition to the (considerable amount of) code review and cleanup that remains to do, there is a potentially lot of interesting commentary to be written, to help the world understand this large formal artifact.

[Bryan Wang]

Probably I am stating the obvious here, but I would add that formalization (and mathematics in general) is not a zero-sum game, so there are still some differences with AlphaZero/AlphaGo.

[Bryan Wang]

But I really like the idea of 'expert analysis' too!

[Jason Reed]

Have we learned anything interesting/novel from this autoformalization effort about what makes a good blueprint, beyond, say, "the more clearly and precisely the outline of the proof is expressed, the better"? Would be very interested to hear if so!

[Kevin Buzzard]

Here is a more precise question: did the autoformalization have to make any new definitions, or were all the key definitions in the proof (for example Schwarz space, modular forms etc) done by humans? This is in some sense a special case of Jason's question.

[Chris Birkbeck]

So I think all of the key definitions were done by humans. Now, its hard to check a ~50k LOC PR, but I asked codex to make a list of the new definitions in the PR (and provided it did it right), it tells me there are 161 new defs, but looking at them briefly, they are mostly basic things, like

@[expose] public def rightHalfPlane : Set ℂ := {u : ℂ | 0 < u.re}

or

@[expose] public def bContourWeight (u : ℝ) (z : ℂ) : ℂ :=
  cexp (π * (Complex.I : ℂ) * (u : ℂ) * z)

[Kevin Buzzard]

Those definitions "need no API" right? They are in some sense making your life worse because the way to prove anything about them is just to unfold them. Although arguably they are useful for organizational purposes.

Are there any definitions made by the autoformalization tool for which some API is developed?

[Chris Birkbeck]

From what I can see, I would say that in general there is no API, but maybe if you are an AI then you don't mind unfolding things all the time. Maybe our future AI overlords will say API is for the weak :joy:

But I did find one place (so far) where it did make some basic API:

/-- The strict width at `∞` for the subgroup `G Γ`. -/
public noncomputable def cuspWidth : ℝ := (G Γ).strictWidthInfty

/-- The cusp width `cuspWidth` is positive. -/
public lemma cuspWidth_pos (Γ : Subgroup SL(2, ℤ)) (hΓ : Subgroup.index Γ ≠ 0) :
    0 < cuspWidth (Γ := Γ) := by
  letI := instIsArithmetic Γ hΓ
  simpa [cuspWidth] using Subgroup.strictWidthInfty_pos (𝒢 := G Γ)

/-- The cusp width belongs to the strict period set of `G Γ`. -/
public lemma cuspWidth_mem_strictPeriods (Γ : Subgroup SL(2, ℤ)) :
    cuspWidth (Γ := Γ) ∈ (G Γ).strictPeriods := by
  simpa [cuspWidth] using Subgroup.strictWidthInfty_mem_strictPeriods (𝒢 := G Γ)

/-- The cusp width belongs to the strict period set of the full level-one group `𝒮ℒ`. -/
public lemma cuspWidth_mem_strictPeriods_levelOne (Γ : Subgroup SL(2, ℤ)) :
    cuspWidth (Γ := Γ) ∈ ((𝒮ℒ : Subgroup (GL (Fin 2) ℝ))).strictPeriods := by
  have hle : G Γ ≤ 𝒮ℒ := by
    simpa [G] using (Subgroup.map_le_range (Matrix.SpecialLinearGroup.mapGL ℝ) (H := Γ))
  have h : cuspWidth (Γ := Γ) ∈ (G Γ).strictPeriods := cuspWidth_mem_strictPeriods (Γ := Γ)
  exact (Subgroup.mem_strictPeriods_iff).2 (hle ((Subgroup.mem_strictPeriods_iff).1 h))

It seems to have made a worse version of docs#Subgroup.widthInfty and then made some API for it. Gauss' version is only for subgroups of SL(2, ℤ) while in mathlib its for subgroups of GL_2 ℝ. So here, while this is maybe a definition you might see in a book, its not as general as our mathlib versions. Doing things more generally than it needs for its current goal is something I think is currently hard for these AIs.

[Martin Dvořák]

Which branch should I be looking at? At the main branch, the main theorem is proved by sorry:
https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean/blob/e708afb5bb9c02aacb0a0ea4ba5e741329ca0d97/SpherePacking/MainTheorem.lean#L5

[Chris Birkbeck]

You want spherepacking#341