Zulip Chat Archive

Stream: maths

Topic: list of mathlib targets


view this post on Zulip Kevin Buzzard (Aug 25 2018 at 11:48):

Over the next couple of days I'm going to have a good look at the perfectoid project from a "bottom up" perspective and try and get a coherent idea of some easy targets for mathlib. For example (although not directly related to the perfectoid project) I would imagine it would be relatively easy to define PID's now and prove that Euclidean domains are PID's and that PID's are UFD's. My feeling is that achievable goals like this should be on some sort of informal list somewhere. Once the p-adic numbers get accepted then defining the adeles of a number field should also be on this list (and if people aren't happy with a definition being on the list then I can propose a random simple theorem about adeles, but for me a definition is fine). Where should such a list live? I remember once, when I was thinking about formalising my graduate course of earlier this year, I thought about formalising the adeles and I made it an issue in mathlib, but now I realise that probably there is a huge list of little things which I'd like to see in mathlib (several of which I'll probably end up doing myself) and I don't think it's sane to have an issue for each of them.

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 11:52):

I should perhaps say that as well as some easy targets I guess I might also end up listing some harder targets. Is there already a place for this? I've realised now that I want mathlib to become the new Bourbaki; that's what people are doing here, and that's the style that they're writing. I think it would be nice to help things along the way by having a list of goals.

view this post on Zulip Johan Commelin (Aug 25 2018 at 12:26):

p-adic numbers are already in mathlib: https://github.com/leanprover/mathlib/pull/262

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 13:08):

I didn't notice that it already got merged! I was just leaving for a holiday the day it did

view this post on Zulip Patrick Massot (Aug 25 2018 at 14:27):

There is https://github.com/leanprover/mathlib/blob/master/docs/wip.md but you can also use https://github.com/leanprover-community/mathlib/wiki

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 14:43):

This is not works in progress -- this is stuff which I want there to be progress on :-)

view this post on Zulip Scott Morrison (Aug 25 2018 at 14:47):

I agree PIDs are gap that needs fixing soon! I've been suggesting my students @Jack Crawford and Ed Hofflin look at those, but as they're still getting started on Lean it may take a while.

view this post on Zulip Scott Morrison (Aug 25 2018 at 14:48):

Let's have a list on the leanprover-community wiki!

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 14:51):

How does that work? If you start something, can other people edit it?

view this post on Zulip Scott Morrison (Aug 25 2018 at 14:51):

I think so --- everyone who has commit access on leanprover-community, and I think the intention is that everyone who wants to make PRs to mathlib can have this.

view this post on Zulip Scott Morrison (Aug 25 2018 at 14:52):

You should try editing the list I wrote for ideas of things to go over next week: https://github.com/leanprover-community/mathlib/wiki/Lean-in-Orsay,-2018

view this post on Zulip Reid Barton (Aug 25 2018 at 14:52):

My first thought would be to just use the github issue tracker. You can organize issues using labels, so I don't think having lots of "feature request" issues would be overwhelming.

view this post on Zulip Scott Morrison (Aug 25 2018 at 14:53):

What if we used issues on the main mathlib repository to indicate defects, and issues on the leanprover-community fork of mathlib for summaries of work in progress, or for wishlists?

view this post on Zulip Reid Barton (Aug 25 2018 at 14:58):

That's possible if that arrangement is clearly signposted somewhere (like, at the top of mathlib's README.md). I do like the idea of including entries for work-in-progress since we're already at the stage at which it can be hard to keep track of what everyone is working on.
Actually, brainstorming small projects of just the sort that Kevin mentioned is on my list of things to do next week, and part of the aim here is to give potential new contributors things to work on.

view this post on Zulip Reid Barton (Aug 25 2018 at 15:01):

For example, Zulip has the "good first issue" tag
https://github.com/zulip/zulip/issues?q=is%3Aopen+is%3Aissue+label%3A%22good+first+issue%22

view this post on Zulip Scott Morrison (Aug 25 2018 at 15:07):

Maybe it does make sense to have them all in one place...

view this post on Zulip Reid Barton (Aug 25 2018 at 15:09):

I'm kind of neutral about it. I do also see the appeal of keeping a separate list.

view this post on Zulip Reid Barton (Aug 25 2018 at 15:10):

BTW, one of the items on my wishlist is the structure theorem for f.g. modules over a PID. Guess I didn't realize there are no PIDs yet either :)

view this post on Zulip Scott Morrison (Aug 25 2018 at 15:13):

Smith normal form is a great project for someone who wants to learn how to do recursion well!

view this post on Zulip Jack Crawford (Aug 25 2018 at 15:24):

Yeah @Scott Morrison I’m pretty keen on tackling Smith Normal Form sometime soon, along with PIDs. (At least, after midsems next week)

view this post on Zulip Johan Commelin (Aug 25 2018 at 17:40):

Someone should also take a serious stab at algebraic closures.

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 18:42):

I'm occasionally pestering @Kenny Lau to do these :-) Kenny -- can you give us an update of what needs to be done?

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 18:43):

I think the issue is that there's some infrastructure which isn't there yet, but I've forgotten what.

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 18:43):

For a while the hold-up was no robust theory of polynomials in 1 variable, but that is now done thanks to Chris.

view this post on Zulip Kenny Lau (Aug 25 2018 at 18:43):

splitting fields

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 18:43):

boggle

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 18:43):

Do you need all the facts about them?

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 18:44):

I mean -- uniqueness? That's the annoying one

view this post on Zulip Kenny Lau (Aug 25 2018 at 18:44):

no

view this post on Zulip Kenny Lau (Aug 25 2018 at 18:44):

we don't even need minimality

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 18:45):

Given a polynomial of degree n over a field K it's not too hard to prove by induction on n that there's a bigger field L contaning K where that polynomial factors into linear factors.

view this post on Zulip Kenny Lau (Aug 25 2018 at 18:45):

yeah

view this post on Zulip Kenny Lau (Aug 25 2018 at 18:45):

right

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 18:45):

Is that tough?

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 18:45):

Oh!

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 18:46):

You need that K[X]/(irred poly) is a field.

view this post on Zulip Kenny Lau (Aug 25 2018 at 18:46):

and you also need to prove that K[X] is UFD

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 18:46):

I don't think you need as much as that

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 18:47):

Do you need uniqueness?

view this post on Zulip Kenny Lau (Aug 25 2018 at 18:47):

no

view this post on Zulip Kenny Lau (Aug 25 2018 at 18:47):

actually we don't need it to be a field

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 18:47):

It suffices to prove we can add a root of a poly to a field and get a new field

view this post on Zulip Kenny Lau (Aug 25 2018 at 18:47):

given f

view this post on Zulip Kenny Lau (Aug 25 2018 at 18:47):

K[X]/(f) is a ring

view this post on Zulip Kenny Lau (Aug 25 2018 at 18:47):

now what do you do with rings

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 18:47):

now take a max ideal

view this post on Zulip Kenny Lau (Aug 25 2018 at 18:47):

you quotient by a maximal ideal

view this post on Zulip Kenny Lau (Aug 25 2018 at 18:47):

tada

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 18:47):

right

view this post on Zulip Kenny Lau (Aug 25 2018 at 18:48):

genius

view this post on Zulip Kevin Buzzard (Aug 25 2018 at 18:48):

I think Chris proved quotient by a max ideal was a field, recently

view this post on Zulip Chris Hughes (Aug 25 2018 at 19:00):

Polynomials are a Euclidean domain is there. I don't think Euclidean implies PID and PID implies prime ideals are maximal is that hard.

view this post on Zulip Kenny Lau (Aug 25 2018 at 19:00):

also PID doesn't imply prime ideals are maximal

view this post on Zulip Kenny Lau (Aug 25 2018 at 19:00):

also s/is/are/

view this post on Zulip Johan Commelin (Aug 25 2018 at 19:04):

Would the following idea be an option. It's a bit of a hack, because of K : Type u, then K-bar : Type (u+1).

view this post on Zulip Johan Commelin (Aug 25 2018 at 19:05):

You let Alg(K) be the type of algebraic extensions of K, and then apply Zorn's lemma.

view this post on Zulip Johan Commelin (Aug 25 2018 at 19:05):

Maybe with some trickery you can even get K-bar back into Type u. I'm not an expert on this.

view this post on Zulip Johan Commelin (Aug 25 2018 at 19:07):

Anyway, whatever the definition, we will want a theorem that says that K-bar is unique up to iso.

view this post on Zulip Morenikeji Neri (Aug 26 2018 at 12:46):

I've actually defined PIDs and have a proof that compiles of ED -> PID (with some help from Chris) @Kevin Buzzard

view this post on Zulip Kenny Lau (Aug 26 2018 at 12:53):

great, now get it to mathlib :P

view this post on Zulip Scott Morrison (Aug 26 2018 at 13:08):

I saw that yesterday!

view this post on Zulip Scott Morrison (Aug 26 2018 at 13:08):

I'm hoping we can bring the proof down to something much smaller. After all, to explain it to a human is only a few lines!


Last updated: May 19 2021 at 02:10 UTC