Tips on looking up theorems...

Stream: new members

[Pietro Lavino]

I am working through the mathematic in lean textbook and I am building a repertoire of theorems I know but those will often lead me to long inefficient and often ugly solution when compared to the provided solution where there is some theorem that does half the work.
I do often try to guess name of theorem after #check to find if there is something relevant, or use "!apply?" but my search is often in vain and inefficient. What is the best process to follow? Thanks in advance

[Chris Bailey]

I think those are still limited by what you have imported/open. The search tool in the doc pages is helpful, and there's a thing called loogle that a lot of people like, though I haven't explored it much.

[Chris Bailey]

Apparently loogle can search by type signature too (I think there's a local/CLI version as well?)

[Kevin Buzzard]

In practice a very efficient way to find theorems about X is to look up the definition of X in mathlib (don't worry if you don't understand the actual definition) and then read what happens next -- it will be a bunch of theorems about X (don't worry if you don't understand the proofs). Perhaps a less intimidating version of this algorithm is to look up the definition of X in the mathlib documentation https://leanprover-community.github.io/mathlib4_docs/ and read what happens next.

[Ralf Stephan]

This is a main problem for me as a beginner. I found that I needed to think as broad as possible and to use all tools that are even remotely helpful. In addition to what is said above I used searching of the code (i.e., Unix grep), searching the whole of Zulip, asking a detailed question on stackoverflow, or give the same question to GPT-4o (which can be surprisingly helpful at times). In the end, the knowledge is in the code, so reading Mathlib is unavoidable.

[Martin Dvořák]

There are many places where you can ask for help or look up something, but as you just said, the only thing you can ultimately trust is the code.

[Luigi Massacci]

moogle is also very helpful

[Luigi Massacci]

https://www.moogle.ai/

[Kevin Buzzard]

And if you know something about the statement of the theorem you want, then there's loogle

[Jireh Loreaux]

I gave a talk on exactly this topic at LftCM 2024 at CIRM. It was recorded and the video is here: https://library.cirm-math.fr/Record.htm?idlist=1&record=19392446124911106289

[Bolton Bailey]

Feels like this might be a good candidate for a blog post. @Jireh Loreaux would you mind if I used your talk as a basis for one?

[Jireh Loreaux]

That's fine.

[Joachim Breitner]

Just watched that talk, very well done! This should help many contributors. And very happy to see people using Loogle so expertly. In particular the way you find Binet's formula with Loogle is very much how I envisioned people to use it: don't bother getting the precise system right in the search, but just list two concepts that very likely are part of the statement (here fib and sqrt), as that often suffices.

I noticed you didn't use loogle's ability to search by lemma name substring. I guess that's because moogle served you well to find how a concept is called in mathlib. It's a clever combination of the two very different searches.

Having this kind of advice in a (more accessible) blog post would be great, thanks for writing that, Bolton!

[Jireh Loreaux]

Joachim Breitner said:

I noticed you didn't use loogle's ability to search by lemma name substring.

Indeed. I expected that new users would not know what things are called, so substring searches wouldn't be that helpful. I probably should have mentioned it though.

[Jireh Loreaux]

The document I'm walking through there is located here: https://github.com/riccardobrasca/LFTCM2024/blob/master/LFTCM2024%2FUsingMathlib%2FMain.lean

[Joachim Breitner]

Right. As we are collecting tips here: I find substring matches also helpful if I think I know the namespace, e.g. with "List." (which is more specific than searching for the constant List) or "Lean"

[Bolton Bailey]

blog#75

[Joachim Breitner]

I would also put in the advice to search from general to specific. So if you are looking for a theorem about the logarithm, start by searching for log, and then iterate only if the result list is too long, by adding one additional filter at a time or restriction, rather than searching for a very specific pattern (which can easily go wrong, due to overloading, order of parameters, etc.) and then seeing an empty result set.

[Joachim Breitner]

Another loogle trick is

|- (?a : Prop)

to search only for lemmas and

|- (?a : Type _)

to search only for data definitions (from https://github.com/nomeata/loogle/issues/9).

[Bolton Bailey]

@Jireh Loreaux recently pinged me about the blog post draft blog#75 I mentioned above a few months ago. I have done a few more revision passes on it and I think it's basically something I would be happy with publishing. Do people think this kind of post is appropriate for the community blog? If not I'm also happy to publish it somewhere else. Who maintains the blog that makes decisions on what goes up there?