Adding Keywords to search the library

Stream: mathlib4

[Omar Mohsen]

I recently started looking at Mathlib. The hardest thing by far is efficiently finding things.

Are there any attempts at making the library easier to search?

Ideally, would it be possible to add Keywords to theorems/structures/classes, etc which Lean regards as comments but another software takes the list of all keywords and makes them searchable. For example, I want to be able to find Pythagoras theorem by writing Pythagoras theorem. Similarly, I want to search for the Category of rings by typing any of the following "Category Ring(s)", or "Ring(s) Category" instead of guessing "RingCat" (for fun "MonoidCat" doesn't work, only "MonCat" gives a hit).

Also, Keywords help make theorems that lie in the intersection of different topics to be easily searchable.
I was asking myself earlier the following question "Which folder is going to contain normed algebras, is it the algebra, the topology, or the operator algebras folder?"

[Matthew Ballard]

Have you tried moogle.ai ?

[Omar Mohsen]

Matthew Ballard said:

Have you tried moogle.ai ?

You just saved hours of my life !

[Johan Commelin]

Are you also aware of @loogle ?

[loogle]

:exclamation: <input>:1:1: unexpected end of input; expected '_' or identifier