# Zulip Chat Archive

## Stream: new members

### Topic: Intro - David Loeffler

#### David Loeffler (Feb 27 2022 at 08:47):

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 (Feb 27 2022 at 08:53):

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

#### Kevin Buzzard (Feb 27 2022 at 09:07):

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 (Feb 27 2022 at 09:22):

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 (Feb 27 2022 at 09:24):

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

#### Riccardo Brasca (Feb 27 2022 at 09:27):

It's here.

#### Riccardo Brasca (Feb 27 2022 at 09:33):

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 (Feb 27 2022 at 09:34):

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 (Feb 27 2022 at 09:36):

@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 (Feb 27 2022 at 09:49):

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

#### Riccardo Brasca (Feb 27 2022 at 09:52):

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 (Feb 27 2022 at 10:51):

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 (Feb 27 2022 at 12:58):

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 (Feb 27 2022 at 13:00):

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.

Last updated: Dec 20 2023 at 11:08 UTC