Loading connector details…
Loading connector details…
Choose a unique username to continue using AgentHotspot
by oOo0oOo • NLP & LLM
An MCP server that enables agentic interaction with the Lean theorem prover via the Language Server Protocol, providing tools for diagnostics, goals, search and automated proof assistance.
Inspect Lean files, retrieve diagnostics, hover documentation, and the current proof goal at a precise source location.
Search for relevant theorems and definitions using local project search (rg), loogle, leansearch, or premise/hammer-style remote services to find premises for a goal.
Run or compile Lean snippets, try multiple proof attempts, and rebuild/restart the Lean LSP server within a project workflow.
lean-lsp-mcp exposes Lean LSP functionality and a set of local and external search tools (leansearch, loogle, premise/hammer integrations, local ripgrep search) through the Model Context Protocol so LLM agents can inspect files, get goals, hover info, run snippets, and query relevant theorems. It supports multiple transports (stdio, streamable-http, sse), environment variable configuration, IDE integrations (VSCode, Cursor, Claude Code) and project build/restart tooling. The server is MIT-licensed and positioned as a beta research tool to assist automated proof development and Lean project analysis.
Build the Lean project and restart LSP. Use only if needed (e.g. new imports).
Get imports and declarations with type signatures. Token-efficient.
Get compiler diagnostics (errors, warnings, infos) for a Lean file.
Get proof goals at a position. MOST IMPORTANT tool - use often! Omit column to see goals_before (line start) and goals_after (line end), showing how the tactic transforms the state. "no goals" = proof complete.
Get the expected type at a position.
Scores are informational only and provided “as is” without warranty. AgentHotspot assumes no liability for actions taken based on these ratings.