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.