Is there a way to search theorems?

Stream: new members

[SL]

Hi, I just discovered Lean and Mathlib. As I understand it, Mathlib is a library of mathematical knowledge, verified in Lean. So my question is, suppose I see a theorem from a "standard" literature (say, a well-known book), how can I know if it is already verified in Lean? I imagine there would be some kind of search engine where you enter the theorem, either the statement itself, or "theorem X in literature Y", and it tells you whether it's in Mathlib or not. Although rare, some good books do contain erroneous results. Also, if you want to add new theorems to mathlib, you need to know if it is there to begin with, right?

I tried to read some portions of the source code, and it was a pain to my untrained eyes.

I am an amateur math lover. Please bear with me if this question is off-topic or trivial. Thanks.

[Rémy Degenne]

#moogle is a website on which you can look for theorems in natural language.
#loogle is for searching using Lean pattern and names.
https://leanprover-community.github.io/mathlib4_docs/index.html is where you will find the whole list of results in mathlib, organized by area (browse the Matblib category on the left). That website has a search bar on the top right.

[Ruben Van de Velde]

If the theorem has a well established name, you should be able to search the documentation Rémy linked to for that as well

[Ruben Van de Velde]

When you get used to the #namingconvention (I hope that links), you may also be able to guess the name

[Ruben Van de Velde]

https://leanprover-community.github.io/contribute/naming.html

[Ruben Van de Velde]

And if you can formalise thestatement of the theorem, you can use by apply?, which might find it

[Ruben Van de Velde]

Occasionally people try to go through a book and formalise the theorems one by one, depending on mathlib for the proofs, but I don't know if anybody started one of those in lean 4

[Ruben Van de Velde]

And last but not least, there's the "Is there code for X?" stream on this zulip, which has the secret weapon Yaël

[Miguel Marco]

A trick that sometimes works for me is to write down the statement and try to solve it by apply?.

[Shreyas Srinivas]

For me apply? rarely works when exact? doesn't. I get a bunch of refine <this and that> which takes me no closer to solving this goal.

[Ruben Van de Velde]

Sometimes it does, sometimes not so much. Depends on what the goal looks like and what the right step is

[Damiano Testa]

I would say "apply? and scan carefully all left-over goals of every suggestion" is much more useful than "apply? and no further processing".

[Ruben Van de Velde]

That for sure!

[SL]

I just typed the statement of the mean value theorem into Moogle. It returns a lot of results, the closest one being Rolle's theorem. Don't know if this means that the mean value theorem is not in mathlib, or if it is considered a simple corollary of Rolle's theorem and thus not worthy of a separate entry.

[Shreyas Srinivas]

SL said:

I just typed the statement of the mean value theorem into Moogle. It returns a lot of results, the closest one being Rolle's theorem. Don't know if this means that the mean value theorem is not in mathlib, or if it is considered a simple corollary of Rolle's theorem and thus not worthy of a separate entry.

https://github.com/leanprover-community/mathlib4/blob/8666bd82efec40b8b3a5abca02dc9b24bbdf2652/Mathlib/Analysis/Calculus/MeanValue.lean#L796

[Shreyas Srinivas]

My search term on #moogle : mean value theorem derivative

[SL]

OK, but most results in a book are not named. I guess that currently, Moogle, or any AI, is still not powerful enough to accurately identify the statement of a theorem with an entry in mathlib. I remember asking ChatGPT a few months ago about theorem 1.1 from a famous book (that has only one edition, so no possibility of confusion; also the book is in ChatGPT's training dataset), and it gave me a completely wrong answer.

[Shreyas Srinivas]

SL said:

OK, but most results in a book are not named. I guess that currently, Moogle, or any AI, is still not powerful enough to accurately identify the statement of a theorem with an entry in mathlib. I remember asking ChatGPT a few months ago about theorem 1.1 from a famous book (that has only one edition, so no possibility of confusion; also the book is in ChatGPT's training dataset), and it gave me a completely wrong answer.

I don't know if Moogle uses ChatGPT's training set. But apart from that, famous or not, books that don't name relevant theorems are really annoying from a practical perspective. An old algebra book did just that and almost cost me an interview. Further, to do such a search reliably the books need to be indexed in many ways.