lean-lsp-mcp has now integrated Lean Finder

Stream: Machine Learning for Theorem Proving

[Wuyang]

Dear all,

We are delighted to share that, thanks to the kind suggestion of Simon Frieder @friederrr from the AIMO Prize, lean-lsp-mcp has now integrated Lean Finder. We greatly appreciate the swift efforts by Oliver Dressler @Oliver Dressler !

You can try it out by entering chat mode in VSCode, Cursor, or Claude Code, typing #lean_leanfinder, and then entering your query (it can be an informal statement, a formal Lean statement, a proof state, etc.). Your chat LLM will then respond using relevant retrievals from Lean Finder as context.

To use Lean Finder, restart the MCP server to get the latest version.

You can find the implementation and description (used by lean-lsp-mcp to brief the LLM) here:

https://github.com/oOo0oOo/lean-lsp-mcp/pull/45

Additionally, the wonderful lean4-skills plugin collection for Claude Code (by Cameron Freer @Cameron Freer ) includes a nice section explaining detailed usage (and so users of the skill do not need to explicitly invoke Lean Finder – it is usually enough to suggest that it be used, and Claude Code will call it with appropriate queries):

https://github.com/cameronfreer/lean4-skills/blob/main/plugins/lean4-theorem-proving/skills/lean4-theorem-proving/references/lean-lsp-tools-api.md#lean_leanfinder---semantic-search-for-mathlib

Happy Lean coding and theorem proving!

Best,

Wuyang

[Timothy Chow]

This is a great tool; thank you!
I tried it out and have already found it useful. However, I did get tripped up a couple of times with recommendations for what seem to be outdated or deprecated names. For example, Lean Finder told me to use Finset.card_insert_of_not_mem which I think is supposed to be Finset.card_insert_of_notMem. On another occasion, it recommended "byCases" which I think is supposed to be "by_cases". Am I doing something wrong or is this just something one has to live with?

[Kevin Buzzard]

If you type Finset.card_insert_of_notMem into https://mathlib-changelog.org/v4 you'll see that it was renamed from ...not_mem to notMem in May, so this is probably an instance of "LLM was trained on an older model of mathlib".

[Wuyang]

Kevin Buzzard said:

If you type Finset.card_insert_of_notMem into https://mathlib-changelog.org/v4 you'll see that it was renamed from ...not_mem to notMem in May, so this is probably an instance of "LLM was trained on an older model of mathlib".

Thank you @Kevin Buzzard for this explanation!

[Oliver Dressler]

Not very elegant, but you can outsource this check to the agent using a prompt like:

Search for theorems on finset cardinality with insertion using the lean finder mcp tool.
Then verify using the local search tool. Check prefixes/alternatives if renamed.

[Alok Singh]

maybe a tool that fuzzy searches by splitting an ident into components, checking different casings and insertions, and seeing if any of those exist

[Oliver Dressler]

Alok Singh said:

maybe a tool that fuzzy searches by splitting an ident into components, checking different casings and insertions, and seeing if any of those exist

Currently trying out improvements to the local_search tool. For the lexical part I'm tending towards BM25S. It should handle some amount of fuzziness.

However, I want to provide pre-built indices/embeddings for all recent toolchains and make sure it runs on a potato. So this will take a little longer.