How to contribute

Stream: new members

[Riccardo Brasca]

Hi to everybody. I am a number theorist and I am quite new to the Lean community. I am reading/viewing various tutorials/videos to understand how it works, but after that I would like to try to prove something that is not already in mathlib. I found this list

https://github.com/kbuzzard/xena/blob/master/many_maths_challenges.txt

Is it reasonable to try to set one of these goals (say in two or three months of work) or it is something very hard? If I start working on some of these problems should I say it here?

Thank you!

[Kevin Buzzard]

Hi Riccardo! I wrote that list. People have been working on Dedekind domains and number fields in the mean time -- there is a thread about them here.

For mathematicians, it's much harder writing definitions of new structures than proving theorems about them, because defining structures is all about implementing specifications, and as mathematicians we're not trained to do that. They typically tell us a way to do ordered pairs in set theory, using the {{x},{x,y}} trick, and leave us how to figure out the rest ourselves.

Group cohomology -- my student finished their thesis so group cohomology can certainly be done, but in doing so I think I learnt a better way to do it -- again this is an implementation issue. it would be hard right now to prove stuff like Hochschild-Serre because abelian categories in Lean have only just appeared, and a tactic for working with exact sequences is being worked on but I'm not sure that it's in mathlib yet.

Galois theory is in full swing. It's pretty much all they talk about in #Berkeley Lean Seminar .

Local fields -- I defined DVRs recently and I think it would be a very interesting project to start getting the basic theory of local fields into Lean. You will be able to get some kind of feeling as to where we are by looking at the (work in progress) file

https://github.com/leanprover-community/mathlib/blob/e80f2799aed8410574ceeec14877e5e1f555ae0e/src/ring_theory/discrete_valuation_ring.lean

In short, we next need to define the valuation on a DVR and prove basic stuff about it. I still haven't decided on the best way to define a local field. There's of course also the issue as to whether we allow R and C to be local fields.

Galois cohomology -- the definition is just group cohomology and then profinite cohomology, and then everything else is way off because it somehow relies on all of the other stuff.

Elliptic curves -- Cremona and I defined the group law on an elliptic curve over k but the equations are so unwieldy that we ran out of memory proving associativity. Of course the correct way to do it is via Picard groups, but we'll get to them later.

Algebra: we now have eigenspaces and generalised eigenspaces. We still don't have the structure theorem for f.g. modules over a PID but it might be the case that @Amelia Livingston will be doing this for her MSc project with me next year -- or did we decide on something else Amelia? Ashvni is doing Iwasawa theory so she'll need the structure theorem for modules over a certain 2-d local ring ($\Z_p[[T]]$) at some point.

Algebraic topology -- I don't know why nobody has defined homology and cohomology of a top space; I'm not an expert in this area and it might be worth talking to others about this.

Representation theory -- I think people are working on this. @Floris van Doorn what's the status of rep theory in Lean?

Modular forms we have essentially nothing. Proving finite-dimensionality might be hard.

On top of all that though, there are schemes. These were defined a week or so ago in Lean and there are plenty of theorems which need proving, for example the fact that Gamma and Spec are adjoint functors from rings to locally ringed spaces. @Kenny Lau you had proved that for the old-fashioned definition -- do you have to start again from scratch with the new definition?

I should tell you that I learnt Lean by doing some undergraduate level stuff and then defining schemes in Lean.

[Amelia Livingston]

We haven't decided yet on MSc project but the structure theorem is at this state currently, 'a few' intermediate sorrys left in 'submodule of free module over PID is free' and 'torsion free over PID implies free'; my first job is to factor out lemmas and document, it's extremely messy rn and some of the functions have profane names

[Kevin Buzzard]

Oh wow you've done tons!

[Riccardo Brasca]

Thank you for the answers! I will have a look about local fields and see if there is something doable! In any case I would be happy to do anything in number theory/algebraic geometry.