Mathlib search

[catalin-hanga]

Can the tool be used on the Mathlib library to search for theorems or lemmas ?

[augustepoiroux]

Hello! No, at the moment LeanInteract does not include such tools in the package. If there is demand for it, I would be happy to include that in though. Feel free to make a PR if you want.