can this be run locally?

[alok]

The rate limit is kinda annoying and for an RL project I'd rather host it so an agent can use it as a tool.

[siddhartha-gadgil]

This is a client that connects to servers that host searches useful in Lean.

It can be extended to local searches if you have a local server with a JSON API that takes a query and returns matches. This can be configurable. Share a concrete setup and API and we can try to extend (or a PR extending).

[siddhartha-gadgil]

@alok Can you clarify what you want? Looks like #20 may address your issue by letting you point to a local url.