Mathlib: the Missing Manuals

Stream: mathlib4

[Anne Baanen]

I am working on organizing and expanding the Mathlib documentation as part of the Mathlib initiative, to cover all gaps and make sure new contributors can find what they need. We are categorizing them according to the Divio system into learning oriented tutorials (think: a Glimpse of Lean), (problem oriented) how-to guides (think: How to use calc), (understanding oriented) explanations (think: most library notes) and (information oriented) references (think: the API documentation).

I have already gone through and analyzed all the pages on leanprover-community.github.io, so now I would like to ask you:

• What piece of documentation has been invaluable to you?
• Is there a critically missing bit of documentation that we should write as soon as possible?

[Eric Wieser]

https://github.com/leanprover-community/mathlib4/wiki/Monad-map has been extremely useful to me at various points in time; I think having similar graphs for algebraic typeclasses in the documentation would be quite helpful, hopefully in a somewhat autogenerated way

[Eric Wieser]

(we'd probably still want multiple graphs so as not to show everything at once; eg one for algebra, one for order, one for a simplified intersection of the two, ...)

[Chris Henson]

Is there a centralized resource that documents what Mathlib's preferred simp normal forms are?

[Bryan Gin-ge Chen]

I really, really miss the automatic library note, attribute, tactic, command, and hole command pages that doc-gen3 was able to generate for us. We do have the mathlib manual which covers some of the above, but it'd be nice if it were more complete and more closely integrated with doc-gen4 for e.g. cross-links between doc-gen4 docstrings and tactics as well as more automated updates.

[Kevin Buzzard]

When I was learning Lean there were very few resources about anything, and I found the short notes filed under "Documentation" in the box on the left of the community website very useful. Several of these notes were written by Patrick and I in 2018; sometimes I would write something which was OK-ish and then get it up there in the hope that someone else who knew what they were talking about (and I certainly didn't back then) would make it better. Examples: I learnt about conv from https://leanprover-community.github.io/extras/conv.html (which I think Patrick wrote), I learnt about simp from https://leanprover-community.github.io/extras/simp.html (which I think I wrote, although the current version bears no resemblence to my original efforts), the only reference for well-founded recursion was https://leanprover-community.github.io/extras/well_founded_recursion.html for many years (which I think Chris Hughes wrote) etc. These brief "focus on one thing, explain an overview and then details, with lots of examples" documents were things I found very helpful.

Both my undergrads and other people seem to find the tactic documentation for the Imperial course https://b-mehta.github.io/formalising-mathematics-notes/Part_2/Part_2.html very helpful; again it takes one topic (here, a tactic) and does the same thing: overview, more detailed explanation, examples.

[Anne Baanen]

I forgot about the various wiki pages! Bhavik's Formalizing Mathematics notes are also very useful. Thanks for pointing them out!

[Ruben Van de Velde]

Yeah, gathering some of the dozen tactic lists and cheat sheets would be great

[Anne Baanen]

About autogenerating library notes etc pages: is it still worth upgrading doc-gen4 or do we expect Verso to take over in the future?

[Anne Baanen]

Since it is already autogenerating the tactic pages for the Mathlib manual project.

[Bhavik Mehta]

I used to find this page incredibly helpful: https://leanprover.github.io/reference/tactics.html it was essentially always open when I was getting started. I think it's somewhere (in terms of detail) between the page on my maths notes (which was in large part written by Kevin!) and this page https://leanprover-community.github.io/papers/lean-tactics.pdf, but in a way I found very helpful.

[Michael Rothgang]

I library notes become a definition ( :fingers_crossed:), at least we'll have doc-gen include them on the generated page. I would really like references to them in the generated documentation to work. A page of all library notes... is useful, but perhaps less urgent.

[Michael Rothgang]

One thing I'd really like: have a collection of overviews or introductions to particular library areas. Topology, basis calculus proofs, ODEs, differential geometry, algebraic geometry, etc. Some of these exist on the webpage (and might want an update?), others should be written. And we should have a canonical home for these (the mathlib manual, perhaps?).

[Julia Scheaffer]

For me, finding documentation on some of the Mathlib tactics has been difficult, but maybe i'm just not looking in the right places. I wish the mathlib docs had a page similar to the lean reference manual's tactic reference (although more usage examples would be nice :sweat_smile:)

[Anne Baanen]

Are the tactic pages in the Mathlib manual what you are looking for, but with more explanations?

[Anne Baanen]

Or are you looking for a more problem-oriented approach, suggesting tactics to use at specific types of goals, instead of listing each tactic one by one?

[Julia Scheaffer]

Anne Baanen said:

Are the tactic pages in the Mathlib manual what you are looking for, but with more explanations?

I believe that is what I'm looking for. Explanations are always helpful. That page seems a bit more helpful than the lean reference manual (definitely has more usage examples) but seems incomplete in some areas. (the entire category theory section is empty :confusion:)

[Anne Baanen]

The manual definitely needs more love! I'll make sure that is on our wishlist.

[Julia Scheaffer]

Anne Baanen said:

Or are you looking for a more problem-oriented approach, suggesting tactics to use at specific types of goals, instead of listing each tactic one by one?

I think that the problem oriented approach is covered fairly well by the "lean tactic cheat-sheet" documents, but maybe problem-oriented resources for more specific situations would be helpful. I remember when I had a proof situation where i needed to use conv for the first time, figuring out how to use it from the tactic reference was a bit difficult.

Now that I look again, I see there's a section of the lean language reference on using conv so maybe my issue is just figuring out where the resource I need are located.

[Anne Baanen]

I wonder if we should have the Lean reference manual as the first "volume" of the Mathlib manual?

[Vlad Tsyrklevich]

Julia Scheaffer said:

Now that I look again, I see there's a section of the lean language reference on using conv so maybe my issue is just figuring out where the resource I need are located.

There is also a section in TPIL.

[Michael Rothgang]

Maybe the tactic manual can link to the relevant sections of the Lean language reference, as needed? Such as, simp linking to simp normal forms, conv linking to the section on conv, etc.

[Wrenna Robson]

There is no guide anywhere on "what makes for a good proof API". I think there's at least one paper in this for what it's worth :)

[Artie Khovanov]

Maybe not something you can fix but SEO / website discoverability for the Mathlib docs and manual are quite poor

[Dexin Zhang]

Bryan Gin-ge Chen said:

I really, really miss the automatic library note, attribute, tactic, command, and hole command pages that doc-gen3 was able to generate for us. We do have the mathlib manual which covers some of the above, but it'd be nice if it were more complete and more closely integrated with doc-gen4 for e.g. cross-links between doc-gen4 docstrings and tactics as well as more automated updates.

I often see -- see note [xxx] in mathlib4, but I can only find the document for them in mathlib3. Is the document of library note not ported to mathlib4 yet, or am I missing something?

[Anne Baanen]

As far as I can tell, there was one missing porting note, partially-applied ext lemmas, which was fixed in a commit today. If you come across any others, please let me know!

[Dexin Zhang]

Oh! I now find them; I need to search for library_note. I thought there should be a document webpage for notes. Anyway thanks so much!

[Johan Commelin]

There most likely will be such a webpage in the future. But for now, indeed you should search for library_note.

[Jovan Gerbscheid]

I think that a list of all reasonably common tactics, such as https://leanprover-community.github.io/papers/lean-tactics.pdf, is very valuable. The problem with this list is that it's hard to find; it would be much nicer if such a thing was reachable from the mathlib docs. And ideally in such an overview there would be links to read the full doc-strings of the tactics.

[Vilim Lendvaj]

There's https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/

[Niels Voss]

One thing I would like documentation on is a guide which states how to express common mathematical objects in Lean. Typeclasses are not in one-to-one correspondence with algebraic structures, due to trying to make the library as general as possible. In many cases it is not obvious how to express things like Banach spaces. So, I think it would be really helpful if there was a giant table (or a bunch of smaller tables, or whatever makes sense for organization) which looked something like

• "V is a vector space over a field 𝕜" -> {𝕜 : Type*} [Field 𝕜] {V : Type*} [Module 𝕜 V]
• "V is a (not-necessarily complete) normed vector space" -> {𝕜 : Type*}[NontriviallyNormedField 𝕜] {V : Type*} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V]
• "V is a Banach space" -> {𝕜 : Type*} [NontriviallyNormedField 𝕜] {V : Type*} [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [CompleteSpace V]
• "V is a real Hilbert space over 𝕜 = R or C" -> {𝕜 : Type*} [RCLike 𝕜] {V : Type*} [SeminormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V]

where the entries of each table are possible coupled with explanations of why the construction is the way it is (i.e. why we don't have VectorSpace and only have Module, or how to choose between SeminormedAddCommGroup and NormedAddCommGroup, which I don't actually understand myself.
I guess my point is that new members might have difficulty figuring out which mixin typeclasses to use, and this might help them.

Similar tables could be made for topological spaces, or even things that aren't types (like how to declare linear maps and conjugate linear maps).

[Kenny Lau]

to add to that, we can document how we use the language of complete lattice to talk about submodules and ideals

[Yaël Dillies]

In general, we are missing documented examples

[Patrick Massot]

Are people aware of the existence of #mil? It answers a lot of those questions.

[Patrick Massot]

@Niels Voss @Kenny Lau all your examples are covered in #mil.

[Rémy Degenne]

MIL is great and asnwers those questions but it is a book, with the answers scattered among the explanations in the pages. I guess it would be helpful to also have a reference sheet for those.

[Rémy Degenne]

Just like both tactic cheat sheets and longer tactic explanations with examples are both useful.

[Michael Rothgang]

Having per-area guides "here's a phrasebook" (translating English to Lean, like you said) coupled with a gentle introduction (a la MIL) and a theory overview would be great.. You just need a volunteer to create those :thinking:

[Yaël Dillies]

Or, these days, an MI employee? :grinning_face_with_smiling_eyes:

[Jon Eugster]

Btw @Anne Baanen please feel free to take over the repo called "mathlib-manual" and do whatever you'd like with it! Or integrate it into whatever you end up building :)

That was mainly a quick prototype and I would be happy if that got integrated into something more complete and better maintained. I would just wish that the autogenerated "list of all tactics" finds a place somewhere:blush:

[Jon Eugster]

About that list: since the underlying Lean code is instructive on how to get all tactics, it should also be quite straight forward to generate this list in doc-gen instead, and display it somewhere there on the page, if you'd wanted to do that.

[Artie Khovanov]

Jovan Gerbscheid said:

I think that a list of all reasonably common tactics, such as https://leanprover-community.github.io/papers/lean-tactics.pdf, is very valuable. The problem with this list is that it's hard to find; it would be much nicer if such a thing was reachable from the mathlib docs. And ideally in such an overview there would be links to read the full doc-strings of the tactics.

This is incredibly useful and I had no idea it existed

[Asei Inoue]

https://seasawher.github.io/mathlib4-help/

is output of #help command

[Snir Broshi]

I feel overwhelmed by the various types of homomorphisms, each having different but similar syntax, and so I think copying Perl's periodic table of operators for Mathlib would be pretty helpful.

[Snir Broshi]

I feel the same way about typeclasses, but there are probably too many to make a readable diagram.
Although Wikipedia has some useful "diagrams" that I visit often:

• https://en.wikipedia.org/wiki/Group_(mathematics)#Generalizations - A boolean table of properties of the single-operation algebras, from magmas to abelian groups
• https://en.wikipedia.org/wiki/GCD_domain - chain of inclusions from rngs to to domains to algebraically closed fields

[Snir Broshi]

Maybe there's a way to partition the typeclasses graph by categories to make it easy to browse.
For example this complexity classes diagram is hard to parse, but this map of subreddits is clustered into regions which make it easier to digest.

[Matt Diamond]

@Dan Abramov has been pretty vocal re: making Lean more approachable and better documented... I'm curious if he has anything specific to add here

[Bhavik Mehta]

I think a list of the common trace options or other diagnostic / debugging tools could be helpful. (I also think a documented list of all trace options would be useful, but that's perhaps more niche).

[Riccardo Brasca]

Most of my fellow mathematicians would love to see a couple of examples on how to use mathlib to state, and prove, a nontrivial result in their area. I am not talking about new projects, but about things that are already in mathlib but the way they are stated is not always clear.

[Thomas Murrills]

Bhavik Mehta said:

I think a list of the common trace options or other diagnostic / debugging tools could be helpful. (I also think a documented list of all trace options would be useful, but that's perhaps more niche).

Aside, but to this end, it would be great to standardize the names themselves! :) @Michael Rothgang started a thread on this here: #lean4 > Naming convention for trace classes

[Michael Rothgang]

Is there a way to get a list of all currently available trace options?

[Anne Baanen]

Is this for metaprogramming, or a reference page request? (For metaprogramming: look for all docs#Lean.OptionDecl s declared in the environment whose name starts with trace?)

[Michael Rothgang]

My motivation was for "does Lean core have a naming convention for trace classes", to inform the above thread --- i.e., compiling a list by hand is fine.

[Andrew Yang]

I have this file lying around in my local vscode for quite some while now because I don't know where to put it. But I think this might be useful for some people including me.

[Kim Morrison]

Unfortunately there is still significant inconsistency in the trace class names in core. If anyone was interested in doing a survey, and even suggesting a way to improve consistency, we would probably happily adopt it.

[Thomas Murrills]

Note: code for listing all available trace classes is now in #lean4 > Naming convention for trace classes, so as to avoid derailing this thread too far. :)

[Kenny Lau]

A list of all monadic notations might be good

[Michael Rothgang]

This comment #mathlib4 > Style bikeshed: `<| ←` vs. `<|←` @ 💬 contains such a list.

[Michael Rothgang]

(I have not tried to check if it is complete.)

[Michael Rothgang]

Having this list, together with an explanation what these combinations mean, seems very useful indeed!

[Thomas Murrills]

Note that most of the functionalities of these are subsumed by simpler and more readable do notation primitives! :)

Fwiw, the ones I do see used are <$> (map, occasionally used terminally or for Option), <&&>, <||> (monadic versions of Boolean operators), <|> (orElse, though requires consideration of its backtracking behavior, and so explicit combinators are often preferred), and >> specifically for parsers.

The rest are useful if you’re coming from or going to e.g. Haskell (or maybe are specifically studying monads!), but I think we ought to encourage do notation for its readability! :) As such, if we had a list of these, it might be useful to also show the do translation.

[Kenny Lau]

yeah I mainly want the do translation because i don't know anything about the theory but i understand programming

[Michael Rothgang]

In one of my meta PRs, you recently suggested using <- and switching the order over >>=. Perhaps this can also be documented there (and should be added to the style guide in any case).

[Thomas Murrills]

Absolutely! I would very much like to collectively decide on and document a preference for do notation in the style guide instead of relying on convention-by-osmosis. :)

[Michael Rothgang]

Thanks for starting the zulip thread! Let's see what comes out of it :)

[Thomas Murrills]

Link to the thread :)

[Bryan Gin-ge Chen]

Something I thought of while working on #30759:

When we deprecate "named" typeclasses like LinearOrdered(Add)CommGroup and OrderedRing in favor of combinations of more basic typeclasses -- are we (should we be) leaving pointers in the docs to make it easier to figure out the idiomatic way to spell these objects? Should we have a separate page listing these?

[Artie Khovanov]

@Bryan Gin-ge Chen Might be a struggle given that folk can't agree how to spell "linear ordered field"

[Bryan Gin-ge Chen]

Well, after #30759 LinearOrderedField won't even exist anymore, so I think we should try to have something, even if it lays out a few options...

[Michael Rothgang]

The mathlib manual could use an update to mention some new tactics:

• the field tactic (same group as field_simp), and
• by_cases! (same group as by_cases)

@Anne Baanen Can I ping you for this? Otherwise, @Jon Eugster probably can tell us what to do.

[Jovan Gerbscheid]

The website on how to make a Lean project makes people download a Lean nightly from April 2024 (https://leanprover-community.github.io/install/project.html). Do they really need to do that?

[Anne Baanen]

Michael Rothgang said:

The mathlib manual could use an update to mention some new tactics:

• the field tactic (same group as field_simp), and
• by_cases! (same group as by_cases)

I don't have any experience with writing for the manual, so this seems like a good excuse to try it out!

[Anne Baanen]

Jovan Gerbscheid said:

The website on how to make a Lean project makes people download a Lean nightly from April 2024 (https://leanprover-community.github.io/install/project.html). Do they really need to do that?

The goal is to have a minimum working version (for those who installed Lean a long time ago and still default to an old Lean). We should be suggesting one from the past months at least, since there are major upgrades to the new project template. (How does elan select which Lean version to use, anyway?)

[Michael Rothgang]

Probably, looking at past PRs/commits by Jon will tell you at least the basics ("add a new tactic X"). Thanks for trying, this is unglamorous but important work.

[Anne Baanen]

I tried updating the Mathlib manual so we could add the new tactics. It was a painful process because the current design involves copying over partial commits from the leanprover/manual repository (but being careful not to overwrite local modifications). So I decided to instead make a PR turning the files copied over, into a dependency brought in by Lake. @Jon Eugster, what do you think?

https://github.com/leanprover-community/mathlib-manual/pull/8

[Anne Baanen]

Based on the previous PR, I made a bumping PR to update to v4.24.0. Note that field and by_cases! are not included in that Mathlib release yet.

[Jon Eugster]

Looks good @Anne Baanen, thanks. I agree the setup is always a merge-conflict nightmare and your solution should already reduce that significantly.

Ideally everthing would be so far modularised and documented that it would be very little overhead to create a document which "has all the features of the Lean language reference but different content". Maybe that's already the case, idk, I'm not keeping up to date with David's work. But maybe you can ask him for a better setup.

I think from me it's only the "all tactics" code and the content of the few pages there are there, everything is just as it is in the language reference

[Michael Rothgang]

I just realised that the cheat sheet https://leanprover-community.github.io/papers/lean-tactics.pdf is not linked on the webpage at all. I would expect an entry in the menu, maybe.

[Antoine Chambert-Loir]

This cheat sheet is wonderful! (Two remarks. The first one is nitpicking: if trysays “run tac only if it succeeds.”, how can try know that the tactic will succeeds without running it? And the second one is to add the possibility of naming the proofs to generalize_proof.)

[metakuntyyy]

One thing that I like to browse is https://github.com/leanprover-community/mathlib4/tree/master/Counterexamples

In general I think having a reference on basic exercises could be helpful. Here is one example of an exercise that I've challenged myself to prove.

import Mathlib

open Classical in
noncomputable def dirichletFunc : ℝ → ℝ :=
  fun x => if Irrational x then 0 else 1

open Classical in
example (x:ℝ) : Filter.map dirichletFunc (nhds x) = Filter.principal {0,1}:= by sorry

In general I think there would be a benefit if some undergraduate exercises that require computation would be shown. For example, given a matrix A and a solution vector b, determine the solution set. This was an exercise in my linear algebra course that was purely computation.

Further examples of such exercises are:

• A function that is differentiable everywhere, but not continuously differentiable: (x*sin(x))
• A function that is smooth but not analytic $\exp(-1/x)$
  and so on.

[Henrik Böving]

If mathlib4_docs is on the page, should there maybe also be a link to loogle given that its a better search engine?

[Anne Baanen]

Good suggestion! I opened a PR: leanprover-community.github.io#742

[Martin Dvořák]

Would you like to include my short guide How to read Lean on the new webpage?
https://github.com/madvorak/read-lean

Or, even better, would somebody like to write a better exposition to reading Lean for mathematicians, and include the better new guide instead of my guide?

There are so many great tutorials on writing Lean code, yet almost nothing on reading Lean code!
I think it is a pity.
I believe that Lean is an extremely powerful language for communicating math:

• human to computer
• computer to computer
• computer to human
• human to human

[Shreyas Srinivas]

Could we have leansearch.net or a similar natural language search tool integrated? I still find it quicker to search parts of mathlib that I know little about.

[Ching-Tsun Chou]

I would appreciate a gentle tutorial on grind. When my PR's are reviewed and I am shown how a block of proof code can be replaced by a single grind call, I often find the result almost magical. The chapter on grind in The Lean Language Reference is not for the beginners, nor is it easy to search. For example, I was shown the following grind call yesterday:

grind [List.mem_iff_getElem, = _ extract_flatten]

It took me some time to find the reference on =_ and, after reading it, I still don't really understand what it does.

[Chris Henson]

Ching-Tsun Chou said:

I would appreciate a gentle tutorial on grind.

While I know the instructions for adding items include a "Focused on Mathlib" criteria, I think there is room to include best practices for grind in Mathlib as it is starting to be used more. Using the profiler to consider performance, tradeoffs with readability, sensitivity to proofs breaking, etc. are things that have been discussed in reviews but maybe not written down in a single location yet.

[Johan Commelin]

@Martin Dvořák @Shreyas Srinivas You can make PRs to add these to the yaml file: see #announce > Mathlib documentation overview @ 💬

[Martin Dvořák]

Thanks for the link, but really wanted to fish for something better than would replace my tutorial. If nobody else feels like writing a better exposition to reading Lean, I will PR mine.