Moogle discussion

Stream: general

[Jason Rute]

It does ok on my go to example for this sort of thing:

the min of a list is less than the max of a list

I like this example since it isn’t exactly true as stated and the true version isn’t in the library but the relevant lemmas are.

[Jason Rute]

Well it can’t find anything good for “the minimum of a list is in the list”. Still not true without assumptions but is the true version not a theorem in mathlib or Std?

[Jesse Michael Han]

Hey y'all, we just announced Moogle (https://moogle.ai), a semantic search engine for mathlib. It lets you find theorems using natural language, and was built with some of the same techniques we used to create Morph Prover v0 7B. We hope this makes it easier for people with math knowledge but not mathlib knowledge to navigate mathlib.

We're excited to improve it based on your feedback!

moogle-GIF.gif

[Jason Rute]

Oh, I found it. It was the 5th suggestion.

[Jesse Michael Han]

make sure to give it a thumbs up! its rank will move up as we improve Moogle

[Notification Bot]

4 messages were moved here from #announce > Moogle by Kyle Miller.

[Kyle Miller]

(@Jesse Michael Han I saw you created this topic so moved discussion here -- I can try to undo it if that wasn't your intent!)

[Jesse Michael Han]

all good :+1:

[Jason Rute]

You may also want to link to the docs# as well as the code. The docs provide useful meta data like instances and they allow click through navigation.

[Jason Rute]

Maybe you can even get the docs to have “search Moogle” along with “Search” and “Google site search” in the top right corner.

[Jesse Michael Han]

that would be great! i think a Zulip bot would be helpful as well, especially in new-members, where Moogle has already appeared in the wild.

[Jason Rute]

I’m not sure there is really value in showing the proofs of theorems and lemmas. They sort of clutter the output. Also in some cases the output is messed up and gets cut off.

[Jason Rute]

For example the second result here: https://www.moogle.ai/search/raw?q=A%20compact%20set%20is%20closed

[Jason Rute]

No good results for “a + b = 0 -> a = -b”. I remember it is a theorem, but it might be stated for (multiplicative) groups in the code. I bet you are going to have a big problem with theorems that are stated more generally than the user is expecting.

[Junyan Xu]

image.png
looks like a bug

[Junyan Xu]

Declaration mul_eq_one_iff_inv_eq doesn't appear among the results.

[Junyan Xu]

mul_eq_one_iff_inv_eq₀ is the 2nd result but add_eq_zero_iff_eq_neg is the 8th.

[Bentley Long]

thanks for flagging! we will investigate

[Junyan Xu]

This one is probably too challenging but I'd expect a good semantic search engine to find docs#unitInterval.qRight by searching https://www.moogle.ai/search/raw?q=homotopy%20between%20two%20continuous%20maps%20from%20the%20unit%20interval%20to%20itself even though the word "homotopy" doesn't appear in the docstring ... Would certainly requires some mathematical background knowledge.

[Jesse Michael Han]

feedback like this is exactly what we're looking for :pray:

[Jesse Michael Han]

it can be a bit wording sensitive and this can be improved by continuous training over time - for example the definition you linked shows up in the results with most results being aboug homotopies if you rephrase the query slightly

https://www.moogle.ai/search/raw?q=space%20of%20homotopies%20between%20two%20continuous%20maps%20from%20the%20unit%20interval%20to%20itself

[Junyan Xu]

Technically it's a single homotopy though (a homotopy between two continuous maps from X to Y is a continuous map of the form I x X -> Y where I is the unit interval, so if both X and Y are I then it's a map I x I -> I. However qRight doesn't actually contain the proof of continuity, so it's good that Moogle finds continuous_qRight. Maybe "space" works better because the declaration is in the file HSpace? Also note qRight doesn't specify which two maps it's a homotopy between (unlike docs#ContinuousMap.Homotopy), so maybe that's why it can't be called a homotopy proper.

[Joachim Breitner]

Very impressive and very cool!

[Julian Berman]

Does Moogle have a current or planned API? And/or relatedly are there thoughts about what editor integration looks like?

[Jason Rute]

Can one just paste a goal in Moogle and expect it to find the relevant theorem (sort of like gptf could do especially if given the prompt “exact” or “apply”)? So far I tried some simple goals and it wasn’t so good.

[Heather Macbeth]

Hmm, it failed on the first thing I tried: didn't find docs#intervalIntegral.integral_mul_deriv_eq_deriv_mul on a search for "integration by parts", although this appears in a section header right above it and the conclusion of the theorem is pretty close to the traditional paper version of the theorem. (This example was suggested by @Alex Kontorovich yesterday.)

[Jesse Michael Han]

Jason Rute said:

Can one just paste a goal in Moogle and expect it to find the relevant theorem (sort of like gptf could do especially if given the prompt “exact” or “apply”)? So far I tried some simple goals and it wasn’t so good.

i wouldn't expect it to do well at this moment, but doing goal -> premise retrieval is on the roadmap!

[Jesse Michael Han]

Julian Berman said:

Does Moogle have a current or planned API? And/or relatedly are there thoughts about what editor integration looks like?

we will soon make the search available in VSCode with search context informed by open editor windows

[Frédéric Dupuis]

Very nice! Another case to have a look at for fine tuning: on "Cauchy-Schwarz" the first two hits are auxilliary lemmas, and the main result I would have expected (docs#inner_mul_inner_self_le, which is right below the first hit in the code) actually shows up pretty far down the list.

[Frédéric Dupuis]

(Admittedly this might be tricky to fix, since the auxilliary lemma actually has cauchy_schwarz in the lemma name whereas the main one doesn't.)

[Jesse Michael Han]

please thumbs-up the correct hit! this will help us improve the model

[Siddhartha Gadgil]

Moogle seems to only search in Mathli, missing stuff in Lean core and Std, such as "Addition on natural numbers is commutative".

[Scott Morrison]

Yes, including results from Std would be very very useful!

[Joachim Breitner]

Jesse Michael Han said:

we will soon make the search available in VSCode with search context informed by open editor windows

I would expect that the local UI/UX considerations for such a search would be pretty much the same for searching using moogle and Loogle. Maybe there could be a single search tool that can query either service? Happy to adjust the Loogle API if it helps.

[Shreyas Srinivas]

Joachim Breitner said:

Jesse Michael Han said:

we will soon make the search available in VSCode with search context informed by open editor windows

I would expect that the local UI/UX considerations for such a search would be pretty much the same for searching using moogle and Loogle. Maybe there could be a single search tool that can query either service? Happy to adjust the Loogle API if it helps.

Up to a point yes. But most loogle searches are likely to be one-liners whereas moogle handles much larger queries and produces larger results.

[Arthur Paulino]

Idea: Moogle could have an escaping key (such as !) to fallback to Loogle when the user has a clearer idea about what to search and is less reliant on mysterious inner mechanics of AI

Idea2: Loogle could be used as a way to enhance the data that Moogle consumes

In general, I agree with the idea of having a single, standard, search tool entry point. I think that's easier on the community (and also on the developers)

[Shreyas Srinivas]

I am writing the loogle part, but that's because I already have access to loogle's API. I don't see any easy integration of moogle other than as a side panel. Maybe a lean command #moogle is better than a separate GUI element for this.

[Junyan Xu]

Junyan Xu said:

Technically it's a single homotopy though (a homotopy between two continuous maps from X to Y is a continuous map of the form I x X -> Y where I is the unit interval, so if both X and Y are I then it's a map I x I -> I. However qRight doesn't actually contain the proof of continuity, so it's good that Moogle finds continuous_qRight. Maybe "space" works better because the declaration is in the file HSpace? Also note qRight doesn't specify which two maps it's a homotopy between (unlike docs#ContinuousMap.Homotopy), so maybe that's why it can't be called a homotopy proper.

Actually, docs#Path.Homotopy.reparam is a better match that Moogle also doesn't find. It's an actual Homotopy, and even though a Path is a continuous map from I to an arbitrary space X that is not necessarily I, this particular definition is obtained by composing a homotopy between two continuous maps I -> I with a path I -> X, so it's surely quite relevant.

[Junyan Xu]

Probably also a bug: sometimes Moogle gets the namespace but sometimes not
image.png
image_univ_equiv is docs#Finset.image_univ_equiv
query

[Jesse Michael Han]

Joachim Breitner said:

Jesse Michael Han said:

we will soon make the search available in VSCode with search context informed by open editor windows

I would expect that the local UI/UX considerations for such a search would be pretty much the same for searching using moogle and Loogle. Maybe there could be a single search tool that can query either service? Happy to adjust the Loogle API if it helps.

yes, that would be great. one idea could be to use #find syntax as a structured query language on top of semantic search results returned by Moogle. so in this combined API, a list of allowed declaration ids are returned by Loogle in response to an exact substring or unification-based search query, and this is used to filter results from Moogle.

[Matthew Ballard]

Jump to definition for terms in the returned declarations would be nice.

[John Yang]

Building this now! Coming soon

[Shreyas Srinivas]

@Jesse Michael Han : My loogle extension is out there (as a preview to see what is preferred UI-wise). Would it be possible to integrate moogle into it by API access?

[Scott Morrison]

I think this is not the highest priority. Rather than asking for custom work from the moogle people, how about we see if the loogle extension is viable and useful first?

[Shreyas Srinivas]

I am only asking if moogle allows api access already, and if I may personally experiment with it for integration. But yes, let's see if the extension is useful for now.

[Agnishom Chattopadhyay]

Great stuff. I definitely like the no-nonsense UI (no chatbot, no big paragraphs of human text). Besides, figuring out which theorem is where is always a chore, so I think this will be pretty helpful.

How does this work? Are you doing some kind of similarity search on some vector representations?

[Thomas Murrills]

Really cool! :D I noticed that if I searched for simply “Tensor product”, I got TensorProduct.tensorTensorTensorComm, TensorProduct.tensorTensorTensorComm_symm, and TensorProduct.tensorTensorTensorApply as the first results—presumably because of how Tensor-y they are.

Are the thumbs up/down appropriate here? I don’t want to suggest that they’re not related to the tensor product, but I do want to indicate that they’re not what should show up if you just search “Tensor product”!

[Jesse Michael Han]

absolutely, for a given query you should thumbs up a result if you think it should be higher ranked (resp. thumbs down, lower ranked)

[Jesse Michael Han]

for example, for a basic query like "tensor product" it ought to pull up the fundamental definition instead of some API lemmas so feedback like that is definitely helpful!

[Siddhartha Gadgil]

As I suggested last round, I do think part of Lean Core and Std should be covered. For example, try: "Addition is commutative for natural numbers." (it cannot find Nat.add_comm which is in Lean core).

[Jesse Michael Han]

This has been fixed, thank you for the feedback!

image-8.png

[Siddhartha Gadgil]

Jesse Michael Han said:

This has been fixed, thank you for the feedback!

image-8.png

Thanks. This is a great tool.

[Notification Bot]

3 messages were moved here from #announce > Moogle by Yury G. Kudryashov.

[Timo Carlin-Burns]

I can't seem to select the search bar at https://moogle.ai to type anything in. Is it just me?

[David Renshaw]

same here

[Scott Morrison]

It's working for me. (Chrome on mac.)

[Timo Carlin-Burns]

Firefox on Linux for me

[Timo Carlin-Burns]

Chromium on my system does show a cursor. So I guess the site isn't working with Firefox

[Jesse Michael Han]

investigating --- we'll get a fix turned around asap, thanks for flagging!

[Jesse Michael Han]

Timo Carlin-Burns said:

I can't seem to select the search bar at https://moogle.ai to type anything in. Is it just me?

OK this should now be fixed --- please give it a try and let me know if it's still not working

[Damiano Testa]

It works for me now: firefox on linux!

[Shreyas Srinivas]

@Jesse Michael Han : Thanks, the moogle extension looks pretty good and works in a complementary fashion with the loogle extension. I do have one question: What does the "Open Moogle" command do? I tried it a couple of times and nothing seemed to happen.

[Shreyas Srinivas]

Also, a feature request for a dark mode :sweat_smile: