Zulip Chat Archive

Stream: Is there code for X?

Topic: modular forms and Hecke operators

Chris Birkbeck (Apr 18 2021 at 16:02):

So I've been slowly learning some lean by looking at the modular forms code from Kevin Buzzard's birthday repo (here: https://github.com/semorrison/kbb/blob/master/src/modular_forms.lean) and getting it running again. Now I was thinking of going a bit further and trying to not just get the definition up and running but also Hecke operators and hopefully proving that Delta and some Eisenstein series are actually modular forms. Ultimately proving something like multiplicty one would be great.

Given I'm pretty new to this area, I wanted to check if this has already been done/ is being done. I couldn't really find anything, but I also don't know exactly where to look.

Riccardo Brasca (Apr 18 2021 at 16:09):

I think we miss some complex analysis to do anything serious about modular forms

Riccardo Brasca (Apr 18 2021 at 16:10):

But it would be an amazing project

Alex J. Best (Apr 18 2021 at 16:18):

I think @Heather Macbeth and @Alex Kontorovich were working on modular forms or related things recently?

Chris Birkbeck (Apr 18 2021 at 16:19):

@Riccardo Brasca Yes well, I think anything with dimension formulas would be tough as I'm guessing enough complex analysis or Riemann-Roch is still aways away. I was just thinking about seeing how far one can get without them.

Alex J. Best (Apr 18 2021 at 16:22):

branch#modular3 might be the latest. In the file number_theory/modular.lean

Chris Birkbeck (Apr 19 2021 at 09:07):

@Alex J. Best Ah thats very useful thanks! I'll try and talk to them.

Last updated: Dec 20 2023 at 11:08 UTC