Why doesn't moogle show these results for cauchy-schwarz

Stream: general

[Sabbir Rahman]

I moogled for "​cauchy schwarz inequality", and I got the vector space version results. But later I learnt that there are also theorems like Real.sum_mul_le_sqrt_mul_sqrt. This would've been useful for my usecase. But what I'm really curious about is why Real.sum_mul_le_sqrt_mul_sqrt didn't appear in the moogle result. The doc strings clearly mention Cauchy-Schwarz inequality. I thought moogle took doc strings into consideration.

[Shreyas Srinivas]

Hard to say. It’s an NLP tool and it might not have been trained recently enough

[Yury G. Kudryashov]

BTW, do we have a tool that searches in names + docstrings + module docstrings? Or google site:https://leanprover-community.github.io/mathlib4_docs/ is the best option?

[Michael Rothgang]

Search within VS Code?

[Sabbir Rahman]

yes searching works, but I had more trust on moogle to find stuff from docstrings :(

[Kevin Buzzard]

A lot of people are migrating to leansearch.net BTW

[Sabbir Rahman]

Kevin Buzzard said:

A lot of people are migrating to leansearch.net BTW

unfortunately leansearch isn't included in vscode lean extension I think, if it was, would be pretty smooth to use

[Michael Rothgang]

Sabbir Rahman said:

yes searching works, but I had more trust on moogle to find stuff from docstrings :(

I'm a bit confused by that: text search is literally what VS Code search does - if anything, I'd expect an LLM to do worse here.

[Kim Morrison]

I still basically use nothing but regexes in the VSCode search box.

[Yury G. Kudryashov]

I use regexes in git grep + loogle.