Are some theorems and defs in Moogle deprecated?

Stream: new members

[jsodd]

Sorry for another stupid question, but may theorems and definitions suggested by Moogle be deprecated? I was trying to find some way to transform a matrix into a quadratic form, but everything Moogle suggests doesn't exist in my version of Mathlib...

[Eric Wieser]

Can you move that question to a new thread? You should be able to edit the message and change the title

[Eric Wieser]

(or hit ... and move message)

[Notification Bot]

A message was moved here from #new members > How to prove decidability for PosDef? by jsodd.

[Jason Rute]

I think it is all dependent on how often they update and retrain Moogle. (I don't think it indexes in real-time.) You can, of course, bug the developers like @Jesse Michael Han. You could also try one of the other searches:

• https://leansearch.net/
• https://huggingface.co/spaces/dx2102/search-mathlib
• (edit: forgot Loogle) https://loogle.lean-lang.org/

[Henrik Böving]

Note that one of the advantages of Loogle is that it can in fact re-index in real time, at the cost of having a different UI compared to AI based search engines.

[Jesse Michael Han]

it's actually still running an index from November 2023 but we will be rolling out a new version soon!