Zulip Chat Archive

Stream: Sphere packing in 8 dimensions

Topic: Weekly Packathons @ CMU

Sidharth Hariharan (Oct 19 2025 at 19:33):

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 (Oct 20 2025 at 21:45):

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

Sidharth Hariharan (Oct 20 2025 at 22:37):

Currently working on spherepacking#157

Sidharth Hariharan (Oct 21 2025 at 01:00):

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 (Oct 21 2025 at 01:03):

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 (Oct 22 2025 at 21:33):

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 (Oct 23 2025 at 00:19):

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 (Oct 23 2025 at 01:35):

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 (Oct 23 2025 at 08:18):

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 (Oct 23 2025 at 18:41):

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 (Oct 23 2025 at 18:46):

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 (Oct 24 2025 at 22:18):

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 (Oct 27 2025 at 17:14):

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 (Oct 27 2025 at 17:19):

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

Evan O'Dorney (Oct 28 2025 at 01:18):

@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 (Oct 28 2025 at 17:45):

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

Yongxi Lin (Aaron) (Nov 02 2025 at 23:39):

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 (Nov 03 2025 at 14:22):

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 (Nov 03 2025 at 14:38):

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

Sidharth Hariharan (Nov 03 2025 at 16:03):

Zoom just crashed, sorry!

Sidharth Hariharan (Nov 10 2025 at 15:24):

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 (Nov 17 2025 at 06:33):

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 (Nov 24 2025 at 13:50):

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 (Dec 01 2025 at 15:35):

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!

Last updated: Dec 20 2025 at 21:32 UTC