Loogle vs. Moogle

Stream: lean4

[Dean Young]

I am new to Loogle and Moogle. Are these very different from each other? Are they for different purposes?

[Thomas Murrills]

They both help you find Mathlib/Std/core definitions and theorems, but they’re for different kinds of search queries!

If you know specific things about what you’re looking for, like the actual structure of the type or hypotheses as a Lean expression (e.g. _ + _) or a substring of the name, loogle can help you find it. Loogle takes advantage lean’s metaprogramming capabilities to actually match on the type and lemma name.

Moogle, on the other hand, is for fully natural-language queries, and uses machine learning to help you find relevant definitions and theorems by description. This is useful when you don’t actually know the Lean/Mathlib form of what you’re looking for yet.

[Eric Wieser]

I think the water is muddied by the fact that moogle has added support for using loogle-style searches

[Shreyas Srinivas]

Querying on moogle in the loogle-style doesn't give you suggestions yet if there are no loogle search hits

[Thomas Murrills]

Oh, I wasn’t aware of that. Do they actually use loogle behind the scenes for that style of search? Or are there differences?

[Eric Wieser]

My understanding is that they just filter the results of loogle (or rather, #find)