Using Loogle in Nvim

Stream: new members

[Michael Novak]

I'm a new user, so I'm sorry if this is a stupid question:
I installed the telescope plugin for nvim and now I'm able to search loogle by the :Telescope loogle command, but when I find something how can I look into it? If I click it with the mouse it seems like nothing happen. How can I see the details, besides just the name that I found?

[Julian Berman]

The slightly easier way which works both in VSCode and in lean.nvim is to use the nice LeanSearchClient API by Siddhartha Gadgil . If you type

import LeanSearchClient
#loogle "Real.sin"

you'll see:

Screenshot 2025-08-30 at 08.40.51.png

Note that this requires being in a project which depends on that helper library, and Mathlib is certainly one of those, so if you're still reading #mil you should be ok to use that.

[Michael Novak]

O.k, thank you very much! What is the benefit of using this over searching loogle with the telescope plugin?

[Julian Berman]

Essentially that it has the same core interface as using leansearch, (which you get from #leansearch "there are infinitely many primes."), one maintained across all Lean editors

[Julian Berman]

the telescope interface does work, though it could use some TLC that I don't have time for yet, if you have issues you likely should scan the telescope docs a bit, you should see both the results from loogle and a preview window with what the theorem found looks like