Beginner Projects

Stream: new members

[Steven Rossi]

Anyone have good recommendations to try implementing in Lean? I want to try contributing to mathlib, and primarily do algebraic number theory, so if there's anything someone needs in that field I'd be happy to attempt it :)

[Yaël Dillies]

There's always https://github.com/leanprover-community/mathlib/issues?q=is%3Aissue+is%3Aopen+label%3Agood-first-project, but nothing in algebraic NT per se.

[Paul Lezeau]

@Steven Rossi I can suggest some things if you want !

[Steven Rossi]

Yeah I took a look at the open issues, but saw that there is a almost done project on number fields in the projects section.

[Steven Rossi]

@Paul Lezeau I'd love to hear it!

[Paul Lezeau]

So a while back I proved the Dedekind-Kummer theorem and it's now on mathlib, but there are a few extra things that would be nice to have. For instance, the theorem is stated by defining a bijection between the prime factors of $p \mathcal{O}_K$ and the irreducible factors of the reduction mod $p$ of the minimal polynomial $f$ of a primitive element $\alpha$ for the extension $K/ \mathbb{Q}$ (strictly speaking the theorem has been done in more generality, but that's not super important), but I haven't yet proven that the bijection is given by taking a factor $\bar{\pi}(X)$, lifting it to a polynomial $\pi(X)$ over $\mathbb{Z}$ and then sending it to the ideal $\langle p, \pi(\alpha) \rangle$.

[Paul Lezeau]

I think it would be a nice little project, and definitely something that would need to be done at some point!
There's a mini todo list around that theorem at the top of this file which I am planning on tackling, but feel free to do some of the stuff there if you feel like it (also the first item of the list is no longer part of the todo list)

[Steven Rossi]

Great, I'll take a look :)

[Adam Topaz]

Do we have the unit theorem yet?

[Yaël Dillies]

Dirichlet unit theorem? @Xavier Roblot has it and progress was unlocked yesterday with the Minkowski convex body theorem hitting mathlib.

[Paul Lezeau]

Oh that's awesome!

[Adam Topaz]

Anyway, there are a million projects in number theory that could be done. Krasner’s lemma is another one that comes to mind

[Alex J. Best]

Yeah I feel like local fields are lagging behind global fields by now!

[Kevin Buzzard]

What's the status of FLT for regular primes? That's a big project which I'm sure could do with some help.

[Kevin Buzzard]

What's the status of FLT for regular primes? That's a big project which I'm sure could do with some help.

[Kevin Buzzard]

Maria Ines was talking about doing local CFT via Lubin-Tate formal groups, but I think she's been distracted by B_{cris}.

[Kevin Buzzard]

What's the status of FLT for regular primes? That's a big project which I'm sure could do with some help.

[Kevin Buzzard]

Maria Ines was talking about doing local CFT via Lubin-Tate formal groups, but I think she's been distracted by B_{cris}.

[Yaël Dillies]

:point_up: How it feels like to be in the same room as Kevin

[Kevin Buzzard]

I'm on an aeroplane! Sorry :-)

[Yaël Dillies]

FLT regular is currently paused because of the port.

[Eric Rodriguez]

but we are fully done with case I and I've got some eyes on the proof of case II

[Adam Topaz]

@Kevin Buzzard my student @Coleton Kotch is doing some work toward Lublin-Tate formal groups right now.

[Adam Topaz]

Just writing down the definition of a formal group is a nontrivial task!

[Riccardo Brasca]

FLT regular is indeed paused, but anybody can of course contribute to it. We can probably write down some relatively easy lemma needed for case 2.

Also, we are still missing a definition of the relative discriminant as an ideal, and a definition of the discriminant for number fields (currently it depends on the choice of a basis).

[Kevin Buzzard]

My feeling is that FLT-regular could be a great guidance for where we want to go with algebraic number theory. If we still don't have discriminant of a number field then it seems that there is plenty of low-hanging fruit -- for example we should really have different and discriminant for an extension of number fields (or perhaps of general field of fractions of Dedekind domains -- my memory is that e.g. differents exist in some huge generality, perhaps you need some lci assumption? There are notes by Conrad and maybe Brinon on this stuff perhaps?

[Riccardo Brasca]

We have the discriminant of a family of vectors, and all that is needed to define as an ideal.