Zulip Chat Archive

Stream: maths

Topic: list of mathlib targets

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.

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.

Johan Commelin (Aug 25 2018 at 12:26):

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

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

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

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 :-)

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.

Scott Morrison (Aug 25 2018 at 14:48):

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

Kevin Buzzard (Aug 25 2018 at 14:51):

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

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.

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

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.

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?

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.

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

Scott Morrison (Aug 25 2018 at 15:07):

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

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.

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 :)

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!

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)

Johan Commelin (Aug 25 2018 at 17:40):

Someone should also take a serious stab at algebraic closures.

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?

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.

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.

Kenny Lau (Aug 25 2018 at 18:43):

splitting fields

Kevin Buzzard (Aug 25 2018 at 18:43):

boggle

Kevin Buzzard (Aug 25 2018 at 18:43):

Do you need all the facts about them?

Kevin Buzzard (Aug 25 2018 at 18:44):

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

Kenny Lau (Aug 25 2018 at 18:44):

we don't even need minimality

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.