Weekly Packathons @ CMU

Stream: Sphere packing in 8 dimensions

[Sidharth Hariharan]

Hi everyone, I'm happy to share that I am running a weekly 'Packathon' (thank you @David Renshaw for the name!) at the Hoskinson Center at Carnegie Mellon, where people here who are interested in the project will be getting together to 'pack spheres', if you will. The packathons will essentially be brainstorming sessions to tackle various project TODOs.

We will resume tomorrow (and reconvene every Monday thereafter till the end of term) at 17:30 Eastern Time ( 2025-10-20T17:30:00-04:00 ). We expect to be working in-person, but if anyone who isn't local would like to join us, the room has a fantastic Zoom setup - just send a message here and we can sort it out! If there is sufficient demand from other timezones, we can consider rescheduling to an earlier time. The whole thing is intended to be quite informal.

Local or not, hope to see you at a packathon sometime soon!

[Sidharth Hariharan]

https://cmu.zoom.us/my/sidharth.hariharan

[Sidharth Hariharan]

Currently working on spherepacking#157

[Sidharth Hariharan]

Thanks to everyone who showed up today, both in person and remotely! Great work - glad we managed to get spherepacking#165 merged and make progress on spherepacking#157 and spherepacking#119.

[Sidharth Hariharan]

Starting next week, we will aim to move the packathons to a more convenient time for anyone wishing to participate remotely from the UK and Europe (though we will probably stick to Mondays unless there is significant demand to move to another day). The virtual component of the meeting will almost always be hosted at https://cmu.zoom.us/my/sidharth.hariharan. I'll repost the link closer to the next meeting.

[Sidharth Hariharan]

Starting next week, we'll do 11 am (2025-10-27T11:00:00-04:00). We will meet in the Hoskinson Centre (Baker Hall 139) and on zoom at https://cmu.zoom.us/my/sidharth.hariharan. Hope to see even more people next week!

[Moritz Doll]

Sidharth Hariharan said:

Currently working on spherepacking#157

Hi, I don't have time to join the meeting, but could you explain how that Fourier transform differs from the one in mathlib and why you cannot just apply docs#Real.tsum_eq_tsum_fourierIntegral

[Bhavik Mehta]

That lemma is a sum over Z, whereas the project needs the sum over Z^n (or perhaps over any lattice in R^n)

[Moritz Doll]

There is a rather slick proof of the Poisson summation formula using distribution theory (Thm 7.2.1 and 7.2.2 in Hörmander 1) and modulo a variant of convolution and some very easy results, we have all of the necessary ingredients. This proof should work directly for any lattice (I don't see why it wouldn't), but I can check that later if you want. The only catch is that it is rather annoying going from Schwartz functions to anything else, but sphere packing uses only Schwartz functions, but that would mean that it is necessary to prove that the special function is in fact Schwartz.

[Sidharth Hariharan]

Thank you for the suggestion! We have been following the proof of Theorem 3.2.8 in Classical Fourier Analysis by Grafakos that seems a bit more elementary, but I am not sure if that really is the case. It requires us to prove some dependencies, but these dependencies seem like useful generalisations of mathlib results, so it's an opportunity for a bit of library building.

[Sidharth Hariharan]

Admittedly I am no expert, but per my understanding, we cannot really avoid proving that the magic function is Schwartz - indeed, it is a fundamental idea that is also necessary for other aspects of the proof. For instance, to show that the Fourier eigenfunctions that make it up are, indeed, Fourier eigenfunctions, we need to show that the Fourier transform permutes the integrals that make it up (with a sign change in the case of the $-1$-eigenfunction). The reason this shows the eigenfunction property is that integrals are themselves Schwartz, so the Fourier transform acts linearly on them. So I feel like proving that the Poisson summation formula is applicable to the magic function is not enough: I think Schwartzness is more intrinsic to the proof.

[Sidharth Hariharan]

Hi everyone!

Next Monday exceptionally, the project maintainers, myself included, will only be able to attend for half an hour (2025-10-27T11:00:00-04:00 to 2025-10-27T11:30:00-04:00) due to a conflicting commitment. After we leave, the packathon will continue for as long as people would like to stay on, led by @Yongxi Lin (Aaron), who is a fellow PhD student at CMU and the driving force behind the Poisson Summation PR. He will also host the Zoom meeting at https://cmu.zoom.us/j/8325240663.

Happy packing!

[Matthew Cushman]

Hi Everyone, enjoyed joining the meeting today! Just wanted to post here so you all have my zulip id. I'm going to get to the topology chapter of Mathematics in Lean this week and depending on how it goes look at the lemma that Aaron pointed me towards at the end

[Sidharth Hariharan]

Thank you very much for coming along! Glad to hear you enjoyed it. Hope to see you at more of them!

[Evan O'Dorney]

@Sidharth Hariharan After you left today, I expressed interest in taking the $d$-dimensional $p$-series step in Poisson summation. Please confirm whether it's still available.

[Sidharth Hariharan]

Thanks for the interest, Evan! I think it should be available - @Yongxi Lin (Aaron) can you confirm?

[Yongxi Lin (Aaron)]

I didn't subscribe this channel previously so I didn't notice these messages at all. Sorry for that :joy:
@Evan O'Dorney Yes you can go for it! Notice that I changed the formulation of that lemma a little bit yesterday.

[Sidharth Hariharan]

Hi everyone! We will convene as usual at 2025-11-03T11:00:00-05:00 at Hoskinson. Those attending online can join https://cmu.zoom.us/my/sidharth.hariharan. See you in a bit!

[Chris Birkbeck]

I can't make it today unfortunately, but have fun!

[Sidharth Hariharan]

Zoom just crashed, sorry!

[Sidharth Hariharan]

Gentle reminder that this week's packathon starts in about 35 minutes (2025-11-10T11:00:00-05:00)! As usual, we'll meet IRL in Hoskinson and online at https://cmu.zoom.us/my/sidharth.hariharan.

[Sidharth Hariharan]

Hi all! As usual, our next packathon is at (2025-11-17T11:00:00-05:00)! We'll meet IRL in Hoskinson and online at https://cmu.zoom.us/my/sidharth.hariharan.

[Sidharth Hariharan]

Hi all! As usual, we will convene in 2h 10 mins (2025-11-24T11:00:00-05:00) IRL at the Hoskinson Center and online at https://cmu.zoom.us/my/sidharth.hariharan.

[Sidharth Hariharan]

Hi all! As usual, we will convene in 25 mins (2025-12-01T11:00:00-05:00) IRL at the Hoskinson Center and online at https://cmu.zoom.us/my/sidharth.hariharan.

This will be our last packathon of 2025. We will resume at some point in January. Looking forward to seeing you soon!

[Sidharth Hariharan]

Hi all! Happy new year!

Term begins next week at Carnegie Mellon, and I thought we could resume our weekly packathons. I was thinking of moving it from Mondays at 11 am ET to Tuesdays at 10:30 am ET. The first one would be 2026-01-13T10:30:00-05:00 and every Tuesday thereafter at the same time. Does anyone have any conflicts?

The model will, as usual, be hybrid. Anyone based in Pittsburgh is invited to join us at the Hoskinson Center (on the ground floor of Baker Hall at CMU - room 139); for those based elsewhere, we will accommodate you on Zoom at https://cmu.zoom.us/my/sidharth.hariharan. (I will try and resend it every week but if I forget and don't specify otherwise, please use this link.)

While the packathons last semester were largely productive, I want them to be a bit more structured this semester. Every week, I'll and put up a poll with potential project TODOs to discuss. (Feel free to suggest things, by the way.) When Tuesday comes around, we can talk about the topics in order of preference. You can propose a topic for which you already have a proof strategy and want suggestions, or we can try and brainstorm a proof strategy together. I'll post a poll for next week very soon. (And I reiterate - suggestions are very welcome!)

I want each packathon to be structured in the following manner:

1. Overview of weekly progress (≤ 10 mins)
2. Brainstorming based on poll responses (30-45 mins)
3. Live PR review (15-30 mins)

We don't have to be super strict with the timings but it would be nice to keep things efficient. 2 and 3 don't have to overlap, but it's entirely possible they might - we can see how it goes. Also, if someone needs a PR reviewed but cannot stay too long, we can always review their PR first before moving onto brainstorming. The meetings will remain fairly informal - people are welcome to join and leave as they please.

Let's get those spheres packed!

[Sidharth Hariharan]

/poll Packathon Topics (Tuesday 13 January 2026)
Integrability: both complex (spherepacking#237 and remaining TODOs) and real (spherepacking#260) integrability of the eigenfunction integrands
Generalising SchwartzMap.compCLM: Using the Whitney lemma about smooth even functions (spherepacking#277) to show that composing the one-dimensional functions (defined in terms of $r^2$, as in the blueprint) with the norm preserves Schwartzness (spherepacking#176)

[Sidharth Hariharan]

(By the way, anyone is welcome to add a new option to the poll)

[Matthew Cushman]

Hi, I'd like to touch on what we should do with PR #227 on the Whitney Lemma as well. I can give a quick update on the status of what I did prior to break. (reading the topics poll, was #277 intended to be #227?)

[David Renshaw]

I just now published the code that I used to make the animation that I showed in todays meeting: https://github.com/icarm/animate-blueprint-depgraph

[David Renshaw]

To make the actual video, I used OBS to capture my browser window.

[Sidharth Hariharan]

Hi everyone! As usual, we'll mee tomorrow at 2026-01-20T10:30:00-05:00. Those joining online can use cmu.zoom.us/my/sidharth.hariharan.

[Sidharth Hariharan]

/poll Topics - 20 Jan
Integrability: Continue discussion from last week (alternatively, we can work on this offline this week and revisit it next week)
Generalising SchwartzMap.compCLM: Is there a way to prove a version of the Whitney lemma for Schwartz functions (ie, a smooth real even Schwartz function is expressible as a Schwartz function composed with x²)
Poisson Summation Formula: Either reviving spherepacking#157 or doing it from scratch
Sphere Packing Constant = Periodic Sphere Packing Constant: see Issue spherepacking#80

[Sidharth Hariharan]

(Feel free to add to this list!)

[Cameron Freer]

@Sidharth Hariharan: I've made good progress towards @Tito Sacchi's list of requested results that are prerequisites for spherepacking#229 -- see that thread for more details.

As such, I'd be happy to discuss it synchronously tomorrow if that's useful -- but also it's probably a good candidate for offline discussion if that is easier for the two of you.

[Yongxi Lin (Aaron)]

I will most likely only be able to attend the meeting via Zoom, but regardless of whether I present, I’ll start working on spherepacking#157 shortly!

[Sidharth Hariharan]

Hi everyone! Hope everyone in this part of the world is keeping nice and warm! Let's convene tomorrow at 2026-01-27T10:30:00-05:00 as usual, both IRL in Hoskinson and on Zoom at cmu.zoom.us/my/sidharth.hariharan.

[Sidharth Hariharan]

/poll Topics - 27 Jan (feel free to add to the list)
Poisson Summation Formula
Periodic Sphere Packing Constant = Sphere Packing Constant
Integrability

[Sidharth Hariharan]

I'll be travelling all of next week for a personal matter, and I won't be able to make the packathon (not even on Zoom). However, if people would still like to pack away, please feel free to meet without me. You'd need to create a new link.

[Sidharth Hariharan]

Let’s just meet online today - the snow outside my apartment is still being cleared!

[Sidharth Hariharan]

Hi all, no packathon this week!

[Evan O'Dorney]

@Sidharth Hariharan Is there a packathon tomorrow?

[Kevin Buzzard]

I think he might be very jetlagged right now :-)

[Sidharth Hariharan]

Yeah, not to mention I’m coming down with something because of all those rapid temperature changes (-20°C to +30°C to -10°C in just over a week). I’m not feeling good enough for a packathon tomorrow unfortunately…

[Sidharth Hariharan]

Hi everyone! I'm sure you've seen the announcement on #announce > Sphere Packing Milestone. We will have a special packathon tomorrow at 2026-02-24T10:30:00-05:00, in person at the Hoskinson Centre at CMU and on Zoom at cmu.zoom.us/my/sidharth.hariharan, where we will answer any questions people might have and highlight ways for people to help with the remaining consolidation work.

[Sidharth Hariharan]

Thanks to everyone who showed up today!

I thought I'd post a quick summary here about what was discussed.

• spherepacking#341 is too long to merge. We have turned it into a draft PR so it isn't accidentally merged.
• Math Inc will break it up into 3 smaller (draft) PRs: one that largely contains stuff about modular forms (@Chris Birkbeck's review area), one that largely contains stuff about the magic function (my review area), and one that contains stuff about the inequalities (@Seewoo Lee's review area).
• We invite community collaborators to pick (mergeable) theorems from any one of the areas (not across areas please - this would make the review process harder) to review, edit, golf and PR to the repo. When you make the new PR, please add Gauss as a co-author (unless you redo the proof completely or in some other way discard Gauss's contributions entirely).
• Once we merge a Gauss-offshoot PR, Math Inc will rebase the appropriate parent draft PR to incorporate the change.

The idea is we will never actually merge Gauss's mammoth PR or any of the 3 smaller PRs (basically I told @Auguste Poiroux thank you for your time, not interested (just kidding!)). The point is, we will merge smaller, more modular PRs that are easier to review, and keep rebasing the big ones off of these.

This process will probably undergo numerous revisions as it progresses; for now, we're going to see how it goes. In parallel, I will resume reviewing some of the earlier PRs, and if they are better than the corresponding Gauss code, we will merge those instead.

Guidelines for choosing lemmas to PR:

• Choose lemmas that only make progress towards one idea or one goal (or pick a small number of lemmas that show related ideas).
• When PRing a definition, please also include any accompanying API. Ideally also say a word or two about where it is used.
• Remember to include corresponding blueprint changes (eg. \leanok).
• No more than 1000 lines PLEASE. Ideally in the range of a few hundred, definitely not over 1000.

We will reconvene 2026-03-03T10:30:00-05:00, entirely on Zoom at cmu.zoom.us/my/sidharth.hariharan.

[Auguste Poiroux]

Hi everyone!
So I have been trying to split the Gauss PR into three smaller PRs as discussed, but I am facing a few challenges that I believe we should discuss before proceeding:

1. The three areas (modular forms, magic function, and inequalities) are not independent, and in the Gauss PR there are interdependencies on newly introduced content -> splitting that into independent PRs while keeping the build green is difficult
2. module system: files using the module system can't import files that are not using it
3. Lean version difference: v4.27.0 vs v4.28.0

For 2 and 3, I suggest the following: first bumping main to Lean v4.28.0, then having a PR to port the codebase to the module system (as already suggested by @Seewoo Lee in the gauss PR). The three PRs will then be based on top of that.
For 1, I see two routes, but please feel free to suggest any other ideas you might have:

• Route A: we make three PRs as independent as possible, and to make this possible, we introduce theorem / definition placeholders for the introduced interdependencies to maintain the build green with a minimal interface / minimal duplication. We might even consider doing more than three PRs for common files like NormNumI, files in ForMathlib, ...
• Route B: the three PRs build on top of each other: modular forms -> magic function -> inequalities. This is more natural and easier to do, but this slightly defeats the purpose of reviewing these different parts independently + the content from magic function and inequalities can't be merged until the modular forms PR is merged.

Looking forward to your opinions on this!

[Snir Broshi]

Auguste Poiroux said:

For 1, I see two routes, but please feel free to suggest any other ideas you might have

In the packathon the recommendation was to add the dependencies with a sorry, does this not work? It sounds similar to route A but not quite.
Do some parts depend on definitions from other parts, rather than theorems? If so then is it possible to make the theorems that are "exported" from one part to the other not mention their own definitions, and treat the definitions as private to the part that defines them? (because sorrying definitions is problematic, as was mentioned in the packathon)

[Auguste Poiroux]

Yes it should work, just want to make sure that we all agree on the whole plan + a few refinement. If we go this route, I believe first porting the codebase to the module system is necessary as a first step (which I am happy to do automatically if maintainers are ok with that), otherwise each PR will have to independently port the project to Lean v4.28.0 + the module system. I also think that it might be even better to split the Gauss PR into more PRs for common files shared across all three developments (but then once again, it is making all the PRs conditional on the previous ones to be merged, so there is a balance here).

[Chris Birkbeck]

Yes I think we want to first move it to the module system and then we can make the PRs. I also agree that maybe more PRs might be easier and also more useful. In general I think we want to break it up into as many small PRs as we can. We can then decide what "category" they fall into. I think that it will be unavoidable to have chains of PRs with dependencies, but at least this way we can work up the chain.