Oliver Dressler - lean-lsp-mcp

Stream: Lean Together 2026

[Rémy Degenne]

Discussion topic.

[Oliver Dressler]

lean-lsp-mcp_LeanTogether2026.pdf

[David Renshaw]

What is the relation between https://github.com/oOo0oOo/lean-lsp-mcp and https://github.com/project-numina/lean-lsp-mcp ?

[Oliver Dressler]

From what I can see the project numina version is essentially a fork from November to which several tools and extra functionality was added.

I have submitted a PR to update the underlying leanclient, which should provide significant speed gains.