Skip to main content
Glama
oOo0oOo

Lean LSP MCP

by oOo0oOo
OverviewSchemaRelated ServersScoreDiscussions
Python
Hybrid

Server Configuration

Describes the environment variables required to run the server.

NameRequiredDescriptionDefault
LEAN_LOG_LEVELNoLog level for the server. Options are "INFO", "WARNING", "ERROR", "NONE".INFO
LEAN_HAMMER_URLNoURL for a self-hosted Lean Hammer Premise Search instance.http://leanpremise.net
LEAN_LOOGLE_LOCALNoSet to true, 1, or yes to enable local loogle.
LEAN_PROJECT_PATHNoPath to your Lean project root. Set this if the server cannot automatically detect your project.
LEAN_LSP_MCP_TOKENNoSecret token for bearer authentication when using streamable-http or sse transport.
LEAN_LOOGLE_CACHE_DIRNoOverride the cache directory for local loogle.~/.cache/lean-lsp-mcp/loogle
LEAN_STATE_SEARCH_URLNoURL for a self-hosted premise-search.com instance.https://premise-search.com

Capabilities

Features and capabilities supported by this server

CapabilityDetails
tools
{
  "listChanged": false
}
prompts
{
  "listChanged": false
}
resources
{
  "subscribe": false,
  "listChanged": false
}
experimental
{}

Tools

Functions exposed to the LLM to take actions

NameDescription
lean_build

Build the Lean project and restart LSP. Use only if needed (e.g. new imports).

lean_file_outline

Get imports and declarations with type signatures. Token-efficient.

lean_diagnostic_messages

Get compiler diagnostics (errors, warnings, infos) for a Lean file.

lean_goal

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.
lean_term_goal

Get the expected type at a position.

lean_hover_info

Get type signature and docs for a symbol. Essential for understanding APIs.

lean_completions

Get IDE autocompletions. Use on INCOMPLETE code (after . or partial name).

lean_declaration_file

Get file where a symbol is declared. Symbol must be present in file first.

lean_references

Find all references to a symbol (including the declaration). Position cursor at the symbol.

lean_multi_attempt

Try multiple tactics without modifying file. Returns goal state for each.

lean_run_code

Run a code snippet and return diagnostics. Must include all imports.

lean_verify

Check theorem axioms + optional source scan. Only scans the given file, not imports.

lean_local_search

Fast local search to verify declarations exist. Use BEFORE trying a lemma name.

lean_leansearch

Limit: 3req/30s. Search Mathlib via leansearch.net using natural language.

Examples: "sum of two even numbers is even", "Cauchy-Schwarz inequality",
"{f : A → B} (hf : Injective f) : ∃ g, LeftInverse g f"
lean_loogle

Search Mathlib by type signature via loogle.lean-lang.org.

Examples: `Real.sin`, `"comm"`, `(?a → ?b) → List ?a → List ?b`,
`_ * (_ ^ _)`, `|- _ < _ → _ + 1 < _ + 1`
lean_leanfinder

Limit: 10req/30s. Semantic search by mathematical meaning via Lean Finder.

Examples: "commutativity of addition on natural numbers",
"I have h : n < m and need n + 1 < m + 1", proof state text.
lean_state_search

Limit: 6req/30s. Find lemmas to close the goal at a position. Searches premise-search.com.

lean_hammer_premise

Limit: 6req/30s. Get premise suggestions for automation tactics at a goal position.

Returns lemma names to try with `simp only [...]`, `aesop`, or as hints.
lean_code_actions

Get LSP code actions for a line. Returns resolved edits for TryThis suggestions (simp?, exact?, apply?) and other quick fixes.

lean_get_widgets

Get panel widgets at a position (proof visualizations, #html, custom widgets). Returns raw widget data - may be large.

lean_get_widget_source

Get JavaScript source of a widget by hash. Useful for understanding custom widget rendering logic. Returns full JS module - may be large.

lean_profile_proof

Run lean --profile on a theorem. Returns per-line timing and categories. SLOW - avoid on theorems that already hit heartbeat limits.

Prompts

Interactive templates invoked by user choice

NameDescription

No prompts

Resources

Contextual data attached and managed by the client

NameDescription

No resources

Latest Blog Posts

MCP directory API

We provide all the information about MCP servers via our MCP API.

curl -X GET 'https://glama.ai/api/mcp/v1/servers/oOo0oOo/lean-lsp-mcp'

If you have feedback or need assistance with the MCP directory API, please join our Discord server