Theorem search tools

Stream: lean4

[Bernardo Tarini]

Hi everyone! I am new here so sorry in advance if I am asking something naive.

I have been really interested in the lean4 programming language since I did a project a month ago for my university, and I am amused by the potentialities this programming language has to help the life of mathematicians.

Since I've started learning lean I have an Hamletian doubt: Mathlib may become richer and richer, may also cover all the existing mathematics, but if there is not a handy way for the user to get access to theorems they need in specific moments this sounds to me kind of useless.

As far as I now (but I'd like to be corrected if I am wrong) the only way this problem has been approached until now is by following specific naming conventions for theorems on mathlib; and thanks to this naming conventions tools like moogle.ai try to do what they are meant to do.

I was wondering if there is some specific work in progress on the side of "letting humans be able to find easily theorems they need": an approach via key-words/semantic fields associated to theorems (N.B. a key word may be associated to a theorem even if this does not appear in its name!), some kind of AI process to link key words to theorems in such a way that the more the users find a theorem (that they end up to use) by a specific key word, the stronger will become the link theorem-keyword in the "searching for theorems algorithm".

Sorry if these sounds to you as useless doubts and questions but I'd be very glad if anyone could enlight me more about this topic.

Best regards,

Bernardo

[Henrik Böving]

The strongest tool that we have for this job which does not work like moogle is loogle.lean-lang.org. It allows you to search for theorems containing combinations of certain types, patterns in their expressions etc. There isn't really a keyword based system integrated with this but it allows for more predictable targeted search if you know the rough shape of your target.

[Riccardo Brasca]

There is also https://leansearch.net/ that is similar to Moogle.

[Eric Wieser]

It would be great if loogle could learn to search docstrings too

[Jason Rute]

Forgive my ignorance, but what would it mean for loogle to search doc strings?

[Mario Carneiro]

if you write "foobar" then loogle will search for declarations containing foobar

[Henrik Böving]

It already does that right now, looking for doc-strings would additionally make it search for occurences of foobar in doc-strings.

[Jason Rute]

Also Moogle and LeanSearch do way more than just go off naming conventions. Also, Lean Copilot has a lemma lookup feature which tries to find lemmas useful for the current goal. (The keywords here are “premise selection” or “lemma selection”.)

[Mario Carneiro]

Henrik Böving said:

It already does that right now, looking for doc-strings would additionally make it search for occurences of foobar in doc-strings.

sorry I guess it was implied but I meant "declarations containing foobar in their docstring"