thoughts on a search engine for mathlib

Stream: new members

[rzeta0]

One of the things I've become very conscious of over the last few months learning lean+mathlib to do simple maths proofs is the relatively poor ability to find lemmas, theorems and definitions that you don't already know about.

I'm aware of loogle and also moogle. From using both my sense is that loogle does straight forward "text matching" search. I've heard that moogle uses more sophisticated algorithms (AI?!) but that's not what I experience when I use it.

So I did some initial thinking about what could be done to improve the situation:

1. I think a search engine that is designed for searching lemmas/theorems/definitions would be helpful.

• • From a bottom-up perspective that would mean searching for "a power b" and the search engine returning content with "x power y". Variable names should be transparent to this search engine - just one example of an optimisation.
• • From a top-down perspective, it would have an ontological understanding of things like domains (sets, functions, relations, groups, trigonometry, topology, ... ) and also of types eg Nat, Prop etc. I should be able to search for a Nat version of a theorem, for example.

2. Perhaps the source content could be better organised to reflect this ontology better, to make it both (1) easier to navigate, and (2) easier to index. When I see the "topic index" on the documentation pages, it doesn't seem that clearly organised. Similar ideas seem to be sometimes in separate libraries - which is ok, but a conceptual map would bring them together.

I suspect others have thought about this issue a lot more than I have. Perhaps some undergrads have been doing summer projects to build prototypes of such ideas?

[Jireh Loreaux]

rzeta0 said:

my sense is that loogle does straight forward "text matching" search

No, this is not at all what loogle is doing. It's more sophisticated. It searches for terms within expressions. It can also search the text within the declaration name, but that's not it's primary utility.

[Jireh Loreaux]

In fact, I would argue that loogle does most of what you request already.

[Jireh Loreaux]

For example, this finds all declarations which somewhere mention a ^ b where a b : ℕ. There are a lot of hits because this is ubiquitous. Note that the variable names have no effect.

@loogle (?a : ℕ) ^ (?b : ℕ)

[loogle]

:search: Nat.even_pow', Nat.even_pow, and 844 more

[Jireh Loreaux]

This finds things related to Fermat numbers: @loogle 2 ^ (2 ^ (?n : ℕ)) + 1

[loogle]

:search: Nat.fermatNumber.eq_1