modular forms and Hecke operators

Stream: Is there code for X?

[Chris Birkbeck]

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]

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

[Riccardo Brasca]

But it would be an amazing project

[Alex J. Best]

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

[Chris Birkbeck]

@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]

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

[Chris Birkbeck]

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