Intro - David Loeffler

Stream: new members

[David Loeffler]

Hello, Lean people! I'd like to introduce myself. I'm a number theorist at the University of Warwick in the UK, and a former PhD student of @Kevin Buzzard. I've been watching the mathlib project from the sidelines (sideleans?) for a good while, but hearing a seminar talk from @Chris Birkbeck about his work on formalising modular forms in Lean finally tempted me to take the plunge and get involved myself.

I am user "loefflerd" on github -- I'd be grateful if someone could grant me access to the non-master branches of the mathlib github repo.

[Markus Himmel]

Welcome. I sent you an invitation, you should be able to see it at https://github.com/leanprover-community/mathlib/invitations

[Kevin Buzzard]

Hi David! Right now there are people working on group cohomology and the Krull topology and cyclotomic fields, so I think the main obstruction to defining Euler systems is that nobody (as far as I know) is thinking about Frobenius elements or decomposition/inertia groups in global Galois groups.

[David Loeffler]

Hi Kevin! I have a lot to learn before I can formalise things from my own research. As a starter project, I thought it might be fun to formalise a proof that zeta(2) = pi^2 / 6 -- has anyone done this already?

[Riccardo Brasca]

Hi David, welcome! I think @Marc Masdeu did that $\sum \frac{1}{n^2} = \frac{\pi^2}{6}$, let me see.

[Riccardo Brasca]

It's here.

[Riccardo Brasca]

Defining the zeta function is something we really want, maybe at the beginning for $\mathrm{Re}(s) > 1$. We now have a little bit of complex analysis...

[David Loeffler]

Thanks! I see the definitions of Bernoulli numbers are in mathlib, so one can formulate the evaluation of zeta(2n) for all n; but I don't know if there's an argument that works for all n without using analytic continuation of zeta(s).

[David Loeffler]

@Chris Birkbeck 's modular forms repo has code for zeta(s) for Re(s) > 1, but doesn't prove much about it. I've seen a nice argument in a paper of Murty that proves, by induction on n, that zeta has analytic continuation to Re(s) > -n; it doesn't use any contour integration so it might be feasible to formalise that.

[Riccardo Brasca]

In any case if you are looking for something to start with, you can have a look at the open issues.

[Riccardo Brasca]

I think we are pretty close to unlock a lot of not-so-trivial number theory: for example we have the discriminant (of a family of vectors, it would be nice to define the discriminant of a number field, or even better of an extension), we more or less have Minkowski theorem (in @Alex J. Best PR #2819)...

[Chris Birkbeck]

I should say that the stuff I have about the Riemann zeta function is basically what mathlib has as a 'p-series'. But hopefully with the stuff used for Eisenstein series we can now at least prove its holomorphic in the appropriate regions.

[Kevin Buzzard]

David, I absolutely agree that the way to learn how to use this stuff is to find a project and start working on it. There's also the ongoing algebraic geometry work https://github.com/leanprover-community/mathlib/projects/13 . @Chris Birkbeck do we have Hecke operators yet?? Something else that @Johan Commelin has always wanted is a description of the Brauer group in terms of division algebras.

[Chris Birkbeck]

Not yet. We'll soon have double cosets and then I plan to add hecke algebras and such. This should hopefully happen alongside me PRing this modular forms stuff.