Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

Topic: What queries do you type in Moogle/LeanSearch?

Nikola Petrov (May 08 2025 at 12:57):

Hi everyone,

I’m working on a project involving information retrieval for Mathlib and have a couple of quick questions for Mathlib users of all levels of expertise:

What kinds of queries do you typically type when searching for declarations using tools like Moogle or LeanSearch?
Any examples of your usual search patterns, whether partial names, informal keywords, or incomplete types, would be extremely helpful.

To be clear: I’m not collecting responses as training data. My aim is simply to better understand the range and style of real-world queries, so I can generate more realistic synthetic examples for evaluation purposes.

Thanks in advance for any insights!

Bolton Bailey (May 08 2025 at 22:31):

Frankly I use a variety of styles of queries. If I'm looking for a nonspecific declaration I might use a phrase or clause. But I've also recently replaced the docs with leansearch for generic searching for specific declarations which I know exist, but that I might not remember the exact name for. In these cases, I usually just search for my best guess at the name and hope that gets me there (I have to worry less about getting the order of parts of the declaration name wrong this way, I think).

Here is a list of the leansearch.net queries in my browser history:

Jason Rute (May 09 2025 at 00:28):

Maybe I'll also copy my history at some point, but in general I often search for:

Names of concepts or theorems: "almost everywhere continuity", "Cauchy Swartz"
Facts in English, "the unit interval is measurable"
Facts in lean without binders: "n + 1 <= m if n < m"
Exact lean identifier I know or think exist: "List.sum"
Lean concepts that may exist: "Finset induction"

Nikola Petrov (May 12 2025 at 14:03):

Thank you for sharing, @Jason Rute and @Bolton Bailey! This makes a lot of sense.

I was also wondering if you sometimes search using equations typed in LaTeX, for example, if you are working on translating a LaTeX proof to Lean?

Bolton Bailey (May 12 2025 at 23:21):

Not really, I think usually latex has a bunch of variable name choices that wouldn't make sense to a semantic search tool.

Jason Rute (May 12 2025 at 23:36):

I'm usually too lazy to use LaTeX.

metakuntyyy (May 20 2025 at 18:13):

My recent queries were something like.

sticks and stones
stars and bars
cyclic unit

This pointed me to the right results.

Last updated: Dec 20 2025 at 21:32 UTC