mathlib overview

Stream: general

[Rob Lewis]

So we have this mathlib overview on the website that's now six months old. Mathlib has grown 40% in that time, surely there's something to be added. Do we have someone responsible for keeping that page up to date?

[Patrick Massot]

This is not the only issue, we also need to think harder about the integration with https://leanprover-community.github.io/undergrad.html.

[Patrick Massot]

I think we should use the infrastructure of the undergrad list also in the general list.

[Patrick Massot]

One possibility would be to add a tag "undergrad" to https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml somehow.

[Patrick Massot]

But I fear it would make that file more complicated, whereas it was designed to be very easy to edit.

[Patrick Massot]

We could also have another yaml file for advanced stuff, but combine both sources when we want to see everything.

[Patrick Massot]

But of course the easiest thing to do is to simply keep two lists, both based on the same kind of yaml.

[Patrick Massot]

There would be duplication between the yaml files, but this is not necessarily bad. The non-undergrad file wouldn't have empty entries, and it would refer directly to the general versions (uniform spaces...).

[Patrick Massot]

Note that we have a clear deadline for people who find motivation in deadlines: it would be nice to clean this up before LFTCM

[Rob Lewis]

That all sounds great. I think the exact details are less important than establishing a routine of keeping it updated, in whatever form it appears.

[Patrick Massot]

The details are important because we need someone to work on the infrastructure and port the current list before we can hope to maintain it.

[Patrick Massot]

And I really need to come back to sphere eversions now that my 5 Heine PR are in the pipeline.

[Patrick Massot]

With the workshop coming really soon, I've had a go at refactoring the mathlib overview. It's mostly the same technology as the undergrad overview, based on overview.yaml which has no formal relation to the original file renamed undergrad.yaml. Those two databases have too different points of view to be reconciled in a sane and convenient way. It also uses theories_index.yaml to link to our detailed theory pages. Note that I took the opportunity to explore using a flat webpage view instead of fancy accordions.

[Patrick Massot]

Hopefully I didn't remove anything that was on the old page. Of course any such list of topics has weird classification issues, but I hope it's useful anyway.

[Patrick Massot]

What would be very useful would be to have a look and quickly add missing stuff (quickly means before Monday).

[Johan Commelin]

@Patrick Massot Wow! That seems like you did quite a lot of YaMLing! Thank you so much :thank_you: :tada: :octopus:

[Heather Macbeth]

This looks great! A couple of minor points: (1) mathlib has the definition and basic properties of analytic functions; (2) links in the line "Measures and integral calculus" are broken.

[Patrick Massot]

Thanks Heather, the measure theory part was completely broken due to an indentation issue.

[Patrick Massot]

I added fractional ideals and analytic functions that I missed.

[Patrick Massot]

A much less urgent question is how people compare this flat view to the fancy view of the undergrad page. Of course both could be tweaked in various ways, the main is to decide whether we should hide stuff by default or display everything at once.

[Johan Commelin]

I think this version is very clear.

[Kyle Miller]

That's nice! I like the flat view because it's less clicking to get a full overview.

It reminds me of the Guide pages from Mathematica's documentation. (Speaking of which, it would be cool if there were Mathematica-style documentation for mathlib. Each definition there has a short description, details and options, many categories of examples, related definitions, and links to related tutorials and guides. Though I understand this would be a tremendous undertaking!)

[Kevin Buzzard]

I think all the infrastructure is there to make this though. You can just add better docs for your favourite theorem, definition or tactic if you're in the mood.

[Bryan Gin-ge Chen]

Yes, and doc-only PRs are very welcome!

[Scott Morrison]

Thanks, @Patrick Massot! I made a PR explaining how to contribute updates to this page.

[Yaël Dillies]

@Patrick Massot said:

Yaël Dillies Let’s think of something you like. Say someone wants to know what kind of combinatorics is in Mathlib, and get some entry points to explore this area. Do you think this page will help them?

Tada: #18884

[Patrick Massot]

Nice! Is it possible to expand the acronyms? Or do you think anyone interested in those lines will more easily recognize the acronyms?

[Kevin Buzzard]

I think LYM is standard (at least I was taught it in Cambridge, but Cambridge might have its own conventions and Yael/Bhavik went through the same system). I've never heard of VC dimension though.

[Bhavik Mehta]

In my opinion these are reasonably recognisable for people interested in these areas, and in both acronym cases it's the first thing that comes up on searching. But I'm potentially biased, and happy either way

[Damiano Testa]

I knew neither acronym, but it is true that a google search revealed what they were.

[Frédéric Dupuis]

VC dimension is definitely well known, at least enough for me to know it despite the fact that I don't work in that area.

[Yaël Dillies]

FYI I already removed an acronym which was quite obscure ("e-transform"). The ones that are left I believe are well-known

[Notification Bot]

7 messages were moved here from #general > stacks tags by Johan Commelin.

[Patrick Massot]

The question is: does it cost something to expand the acronyms? Sometimes people simply don’t know what some acronym stand and don’t recognize the expanded version.

[Shreyas Srinivas]

Vapnis-Chervonenkis Dimension is not more informative

[Patrick Massot]

This is not the question I’m asking.

[Patrick Massot]

I want to know whether it is less informative.

[Shreyas Srinivas]

Oh you mean have the standard abbreviations and the expansion?

[Patrick Massot]

By default, we don’t use abbreviations. So expanding the abbreviation is the default thing to do. But I don’t want to ask this if it makes those lines harder to read for people who care about combinatorics.

[Daniel Weber]

Patrick Massot said:

I want to know whether it is less informative.

It might take a few seconds to recognize, if it's not the commonly used name, but I don't think more than that, especially with context

[Luigi Massacci]

I remembered "VC dimension" as is from a statistical learning class, but if I saw it spelled out with the names it would have taken me more time, with the extra step in my head being conversion back to the acronym

[Patrick Massot]

Ok, let's keep the acronym then.