Zulip Chat Archive

Btw, https://github.com/leanprover-community/lean/ needs a better explanation what it is, and what the differences are with the official released Lean

Mario Carneiro (Nov 23 2019 at 01:44):

I'm not sure I can (re: ProvingGround). It's not clear what it has to do with lean though

Mario Carneiro (Nov 23 2019 at 01:45):

I would just remove it unless we can relate it to lean somehow, it looks random / off topic

Mario Carneiro (Nov 23 2019 at 01:46):

I would say "Lean 3 Community Edition is a fork of the frozen Lean 3 repository maintained by the mathlib team"

Floris van Doorn (Nov 23 2019 at 01:48):

Removed / Added

Mario Carneiro (Nov 23 2019 at 01:49):

why is the paper link for Alive in Lean omitted?

Mario Carneiro (Nov 23 2019 at 01:49):

do direct links not work or something?

Bryan Gin-ge Chen (Nov 23 2019 at 01:51):

We could make these subpages of the the site at https://leanprover-community.github.io

Mario Carneiro (Nov 23 2019 at 01:52):

That's a good idea. I would put at least a few of these sections right on the front page

Floris van Doorn (Nov 23 2019 at 01:55):

Yeah, I'm happy to move this to the webpage.

Bryan Gin-ge Chen (Nov 23 2019 at 02:01):

OK, just make a PR here. It's a Jekyll page so I think you can pretty much just add / merge your markdown files with the ones there.

Patrick Massot (Nov 23 2019 at 10:25):

In "Learn Lean", the mathlib tactic writing tutorial is meant to be read before Programming in Lean.
"Papers" using Lean misses at least Mario's computability paper.
"Papers about Lean" and "Lean 4" miss the report on formalizing bean counting.
I don't won't where, but you could mention Paul-Nicolas report about norm_cast

Patrick Massot (Nov 23 2019 at 10:30):

It's nice to see things slowly converging to having a really nice website for the mathlib community with help and all sorts of documentation. I'm really sorry I have so little time to contribute.

Patrick Massot (Nov 23 2019 at 10:31):

see https://lean-forward.github.io/#papers

Patrick Massot (Nov 23 2019 at 10:32):

That's a fancy website by the way. Did Jasmin hire someone to write it?

Mario Carneiro (Nov 23 2019 at 10:38):

At first I thought you meant the faux-lean style used for the first Lean Together conference

Patrick Massot (Nov 23 2019 at 10:38):

No, that's a new one.

Mario Carneiro (Nov 23 2019 at 10:40):

We need to get whoever did that webpage to help with the mathlib web pages

Patrick Massot (Nov 23 2019 at 10:40):

Oh, the paper list also misses Rob's p-adic paper.

Patrick Massot (Nov 23 2019 at 10:41):

That webpage is maybe a little bit too fancy.

Mario Carneiro (Nov 23 2019 at 10:41):

don't underestimate the power of a glitzy web page

Patrick Massot (Nov 23 2019 at 10:41):

This is really purely a propaganda page. We'll need some more technical page. But clearly the mathlib doc is currently unusable on a phone.

Rob Lewis (Nov 23 2019 at 11:39):

That's a fancy website by the way. Did Jasmin hire someone to write it?

Yeah, he paid some graphic designer to do it. (From his own money, so don't worry, we're not spending Dutch taxpayer money on glitzy webpages.)

Rob Lewis (Nov 23 2019 at 11:40):

Floris, this is great, thanks! We should definitely work it into the community webpage. It can replace the bibliography page which is pretty minimal.

Rob Lewis (Nov 23 2019 at 11:40):

Although maybe we should keep and update the .bib file there.

Rob Lewis (Nov 23 2019 at 11:41):

If anyone wants to redesign the community site, that's totally fine with me. I'm not attached to its current style. It's simple and it works.

Kevin Buzzard (Nov 23 2019 at 12:19):

Maybe it's time to put up a list of things which we the community would like formalised. I am often being asked this on Twitter/email: "hey, I liked your game, I'm a mathematician, what needs doing?" I would like to be able to point people to a list and say "here's a bunch of stuff". I am envisaging the list containing everything from projects which a beginner with a mathematical background could think about (e.g. structure theorem for modules over a PID, uniqueness of factorisation of ideals into prime ideals in the integers of a number field, or other 3rd year / 4th year UG algebra stuff which I could probably attempt to supervise via Zulip) to wishlist stuff like Groebner bases which will take an expert. I've realised that I keep thinking of things and I never know where to put them. Maybe now is a good time to think of a place for such ideas and then people will be able to add stuff as necessary.

Rob Lewis (Nov 23 2019 at 12:26):

We could easily add a page to the community site for this. But people have to be willing to keep it up to date.

Kevin Buzzard (Nov 23 2019 at 12:58):

OK I'll take this on. There were some far more primitive "what is in Lean" pages which I wrote two years ago when I was trying to figure out what was in Lean by looking at every file in Lean and mathlib; I wrote some random blog posts but blog posts are manifestly more transient. At some point did these get ported over to some more official place? They will also need updating. But I think it's got to the point where we should have some brief informal descriptions of what we have and some wishlist.

Rob Lewis (Nov 23 2019 at 13:04):

I do think there's a relevant difference between Floris' list and what you're proposing. The list of resources is pretty stable. Individual items may get outdated, and there will be additions, but the list doesn't need frequent updating. Pages on "what's in mathlib" or "what should you work on" need regular attention, or else they'll be misleading.

Kevin Buzzard (Nov 23 2019 at 13:07):

I totally agree. I didn't want to maintain my blog posts but I would be happy to maintain something more official.

Kevin Buzzard (Nov 23 2019 at 13:09):

I am just getting a steady stream of people asking me these questions and instead of just answering them one by one it would be much easier for me to be able to point them to something.

Rob Lewis (Nov 23 2019 at 13:12):

Cool. To add a page to the community site, you just need to add a .md file with the right header. See https://github.com/leanprover-community/leanprover-community.github.io/blob/master/bibliography/index.md for an example.

Mario Carneiro (Nov 23 2019 at 13:44):

How about a really detailed roadmap / wishlist of theorems? Sorted by dependency order, with each individual item being no more than say 100-300 theorems (so no "analysis" item, that's useless). If we just write it as a checklist, then it will be pretty stable going forward, we just check off items as they get done

Kevin Buzzard (Nov 23 2019 at 13:52):

How about we just get started now with some basic ideas and work towards this? But I am happy to have this as a goal.

Mario Carneiro (Nov 23 2019 at 13:53):

For example, here's what I see in undergraduate analysis:

Define single variable derivative
Addition rule, multiplication rule, chain rule
Power rule, derivative of a polynomial
derivative of a limit, derivative of a convergent power series
derivative of complex exponential
derivative of complex trig functions
relating real and complex derivatives, real exponential and trig
inverse rule, derivative of real log
argument function, derivative of complex log
Define integral of nonnegative real functions
Integral of real -> complex functions
scalar multiplication of integrals
addition of integrals
integral upper and lower bounds, derivative of a definite integral (FTC1)
integral of a derivative (FTC2)

Kevin Buzzard (Nov 23 2019 at 13:53):

Out of interest, are you envisaging something more or less detailed than https://github.com/leanprover-community/lean-perfectoid-spaces/issues/33 when you say "really detailed roadmap"?

Kevin Buzzard (Nov 23 2019 at 13:54):

Your list above -- some of these are done, right?

Mario Carneiro (Nov 23 2019 at 13:54):

yes

Mario Carneiro (Nov 23 2019 at 13:54):

we're already on our way to completing the list, good

Mario Carneiro (Nov 23 2019 at 13:55):

also some of the items are not stated in the generality that we may actually want when we get there, but it gives a hint as to the intended application so we should make sure it works in these cases

Mario Carneiro (Nov 23 2019 at 13:56):

for example, integral of functions R -> C is what we need but mathlib is going for some more general notion over vector spaces. That's fine, as long as the theory applies painlessly to R -> C. If it is not painless, then we need to specialize parts of the theory until this use case works

Mario Carneiro (Nov 23 2019 at 13:58):

I would prefer a list that doesn't have an item saying "here's where it gets murky"

Kevin Buzzard (Nov 23 2019 at 14:01):

I would prefer a list that doesn't have an item saying "here's where it gets murky"

Yes Patrick was not fond of that line either. I wrote that in April and Patrick basically told me (correctly) that I was no good at writing roadmaps. The later messages were written in October and unmurkify things.

Kevin Buzzard (Nov 23 2019 at 14:01):

The reason I explicitly linked to it was that the posts I wrote in October were my first serious attempt to write a roadmap without giving up whenever stuff got murky.

Mario Carneiro (Nov 23 2019 at 14:02):

In the case of undergraduate analysis, you can pretty much pick up any calculus book to get the gist of the proofs (although formalization changes things), but at least I wouldn't have enough guidance given only the perfectoid roadmap. This is probably unavoidable for higher level mathematics, but in these cases, some pre-digestion of primary source materials (i.e. "etale cohomology of diamonds") is necessary, and is an important role played by the mathematicians writing the roadmap to prepare the way for "beginner + computer" (to paraphrase de bruijn) to be able to do the formalization work

Mario Carneiro (Nov 23 2019 at 14:04):

For really advanced stuff, you might have to write a full (informal) proof, similar to the book that describes the text part of the flyspeck project

Kevin Buzzard (Nov 23 2019 at 14:51):

I would not imagine the perfectoid roadmap been done by a math beginner, I would envisage it only being done by someone who knows the maths back to front. To be honest I would envisage it being done by either Johan or me, when we get round to it (it's not Patrick's speciality) , so I was really writing it for us. Another possibility is that a PhD student does it with me helping.

I think there are issues here which will only become clearer once I start writing the lists. I don't want to do this today (I want to do real number game stuff) but I do want to do it.

Mario Carneiro (Nov 23 2019 at 15:31):

The roadmap is of course being done by an expert

Mario Carneiro (Nov 23 2019 at 15:32):

the purpose of the roadmap is to make the work of elaborating the roadmap into a proof that of a less-expert

Mario Carneiro (Nov 23 2019 at 15:39):

The thing is, writing careful informal proofs is something that practicing mathematicians already know how to do, and it is an important and valuable part of the formalization process. You don't see this as much at the undergrad level because careful mathematical proofs are copious, but for advanced and complex proofs I cannot stress enough how much difference a careful and straightforward informal proof makes in smoothing over the rough bits of big projects.

Patrick Massot (Nov 23 2019 at 17:00):

We already have roadmaps and wishlists as issues on GitHub, right?

Mario Carneiro (Nov 23 2019 at 17:06):

You could organize a todo list like that using github issues, but they seem a bit coarse-grained; you wouldn't want one issue for each element on that list, so you would have to split it down into topics or something. At least the way I've presented it, it seems like a mathlib .md file would be the nicest way to have a longish list of everything in the near future we care about (I'm thinking something like 100-200 entries total, sectioned according to topic)

Mario Carneiro (Nov 23 2019 at 17:08):

in basically all of my big mathlib projects (dioph, computability, multiset, ordinal) I have a big list like that in my head, and I just check everything off the list, and once I can't think of anything else to add I'm done

Simon Cruanes (Nov 23 2019 at 18:03):

There's the notion of "github projects" which allow one to keep together a lot of cards (some of which can be issues, although it's not necessary) in columns "todo", "in progress", etc.

Johan Commelin (Nov 25 2019 at 08:09):

@Floris van Doorn Thanks for writing this list! I needed something just like that because I will be giving a Lean talk on Wednesday to people who've never heard of it before...

Johan Commelin (Nov 25 2019 at 10:45):

I think these roadmaps would be good to have. They might then also give a clear overview to the "where do we stand" question.

Rob Lewis (Nov 25 2019 at 10:51):

I don't think the main difficulty with these things is where to host them. Pages on Kevin's blog, pages on the community site, GitHub issues or projects or wikis, it's all the same content. As long as it's visibly linked to from important places it will be found. The hard thing is actually keeping it up to date.

Rob Lewis (Nov 25 2019 at 10:51):

This hasn't happened with any of the earlier attempts to do this in any format.

Rob Lewis (Nov 25 2019 at 10:54):

(By "these things" I mean the roadmaps and wishlists. Floris' list will be much simpler to maintain.)

Kevin Buzzard (Nov 25 2019 at 11:48):

At the minute the hard thing is finding the time to write the lists.

Floris van Doorn (Nov 25 2019 at 19:44):

"Papers about Lean" and "Lean 4" miss the report on formalizing bean counting.

@Patrick Massot Do you mean something other than the paper (which is linked)?

Thanks for your suggestions!

Patrick Massot (Nov 25 2019 at 19:50):

I meant @Marc Huisinga's bachelor thesis: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20in.20the.20wild/near/179911868

Floris van Doorn (Nov 25 2019 at 21:07):

Thanks, I added it!

Floris van Doorn (Dec 03 2019 at 00:27):

I moved the list to https://leanprover-community.github.io/links/

Last updated: Dec 20 2023 at 11:08 UTC