Searching in mathlib

Stream: new members

[Walter Moreira]

I saw this discussion on #general: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Undergraduate.20math.20list/near/197327879 and got me inspired to ask about the best practices to search for content in mathlib.

When searching for a given fact, I usually struggle, and specially when I don't know the the level of abstractions with which it was formalized in Lean.

In my dream world statements would be tagged with a set of keywords, and a page could be automatically constructed to query for those keywords. Has there been any discussions to build a kind of ontological system on as a meta-system on top of mathlib? Other than asking about how that, I'd love to hear any advice on efficient searching of mathlib.

[Jalex Stark]

Here's an example.
If you know that you're looking for facts about groups, you either type the word group or look through mathlib for files called group

[Jalex Stark]

if you look through mathlib, you'll end up in either src/group_theory or in something like src/algebra/group/basic.lean

[Jalex Stark]

either way, you'll have a file that gives you one nontrivial statement about groups

[Jalex Stark]

then that is probably enough to teach you how to type the theorem you want and then apply library_search

[Kevin Buzzard]

There are lots of different ways to search, and some work better than others in different situations. @Walter Moreira do you have an explicit example of something you might want to search for?

[Bryan Gin-ge Chen]

We have space for tags in the "module documentation" that's supposed to be at the top of every file in mathlib, but we haven't done too much with those yet.

[Walter Moreira]

@Kevin Buzzard No, I don't have a concrete example at the moment (documentation has been good, and library_search is a magical thing). I just like to think about organization and thought to ask.

[Jalex Stark]

I think this is a good problem to think about, but you should remember that this is also a problem in normal software engineering

[Walter Moreira]

On the other hand, how does library_search works? Does it search for the conclusion of any proposition that matches the one you goal you have?

[Jalex Stark]

So if there are any easy ways to make a lot of progress, they are either specific to theorem provers or already known

[Walter Moreira]

@Jalex Stark I agree. That being common in the engineering world is what was triggering my thinking here.

[Jalex Stark]

Walter Moreira said:

On the other hand, how does library_search works? Does it search for the conclusion of any proposition that matches the one you goal you have?

@Scott Morrison is the expert, I think. In my experience the best way to use it is to try to guess exactly the type signature of the lemma you're looking for, even the order of implications may matter

[Jalex Stark]

I usually have a better time with library search if I extract the lemma from my local context and make it its own example

[Walter Moreira]

As a beginner, my issue so far has been to identify the correct abstraction that's being used in mathlib. For example, if I'm looking for a topological statement, I do need to know that Lean is likely to have it expressed as filters and not as the undergrad-like expression. In that way, I feel a higher level search would be useful.

[Bryan Gin-ge Chen]

One big task is to get all of mathlib up to date with the documentation requirements. Then at least google (which is the search currently built-in to the doc pages) can index math written in English rather than just code.

[Patrick Massot]

Walter, you are totally right this is currently pretty hard. And Bryan is right to point out the documentation task. Note that beginners can help with documentation :wink:

[Walter Moreira]

@Bryan Gin-ge Chen Is there something beginners can help with, while learning?

[Patrick Massot]

See the answer above your message

[Walter Moreira]

Ha! I was just writing that and you beat me :-)

[Walter Moreira]

Is the process for helping with documentation described somewhere?

[Jalex Stark]

I guess by "the process" you mean making PRs to mathlib?

[Patrick Massot]

https://help.github.com/en/github/collaborating-with-issues-and-pull-requests/about-pull-requests ?

[Patrick Massot]

There is also the thread you linked to.

[Patrick Massot]

As well as commenting about and PRing to all our documentation sources (see https://leanprover-community.github.io/learn.html)

[Bryan Gin-ge Chen]

The process might be something like this:

1. read a mathlib file and notice that the documentation is missing
2. checkout mathlib to your computer
3. make a new branch and make edits to the file
4. push the branch to github and then open a PR

We have this file for new contributors: https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/index.md (which should probably be updated to remove the nursery).

[Walter Moreira]

Cool, thanks! I wanted to confirm PRs where the proper approach. Thanks for the details @Bryan Gin-ge Chen