lean-lsp-mcp

You can send Lean 4 code, natural language math problems, or proof strategies to different models
and get their suggestions. This is useful for:
- Discussing proof strategies and approaches
- Getting alternative reasoning paths
- Comparing suggestions from different models
- Debugging stuck proofs

Args:
    question (str): Lean code, math problem, or any question you want to discuss.
    model (str): Choose "gemini" (Google gemini-3-pro-preview) or "gpt" (OpenAI gpt-5.2-pro). Default is "gemini".

Returns:
    str: The model's response.

It uses Google's Gemini API to generate text responses. You need to set the GOOGLE_API_KEY environment variable.

Args:
    lean_code (str, optional): The lean code to be golfed.
    model (str, optional): The Gemini model to use. The default is "gemini-3-pro-preview".
    temperature (float, optional): The generated temperature, controlling randomness. The default is 0.7.

Returns:
    str: Gemini model response or error message

Use Google Gemini model to solve math problems and provide detailed solution.

This tool takes a raw math problem string, solves it, and explains the reasoning step-by-step.

Gemini's math skills are outstanding; you can trust the answers he gives you.

Use this tool frequently for natural language math problems.

You should mention that you’re aiming to formalize the solution in Lean 4, and ask Gemini for a detailed solution that would be easier to formalize.
Once you receive Gemini’s solution, use leandex to search mathlib for relevant theorems and lemmas.
If you discover that some necessary infrastructure is missing in mathlib, immediately switch to informal_prover: provide it with Gemini’s solution, explain what is missing, and ask it to propose an alternative approach that avoids those gaps or requires less infrastructure.

Args:
    math_problem (str): The detailed text description of the math problem.
    model (str, optional): The Gemini model to use. The default is "gemini-3-pro-preview".
    temperature (float, optional): The generated temperature, controlling randomness. The default is 0.7.

Returns:
    List[str]: [solution, verification_result] where solution is the step-by-step explanation and verification_result is the Gemini verification judgment.

Use OpenAI GPT model to solve math problems and provide detailed solution.

This tool takes a raw math problem string, solves it, and explains the reasoning step-by-step.

GPT's math skills are outstanding; you can trust the answers he gives you.

Use this tool frequently for natural language math problems.

You should mention that you’re aiming to formalize the solution in Lean 4, and ask Gemini for a detailed solution that would be easier to formalize.
Once you receive Gemini’s solution, use leandex to search mathlib for relevant theorems and lemmas.
If you discover that some necessary infrastructure is missing in mathlib, immediately switch to informal_prover: provide it with Gemini’s solution, explain what is missing, and ask it to propose an alternative approach that avoids those gaps or requires less infrastructure.

Args:
    math_problem (str): The detailed text description of the math problem.
    model (str, optional): The GPT model to use. The default is "gpt-5.2-pro".
    temperature (float, optional): The generated temperature, controlling randomness. The default is 0.7.

Returns:
    List[str]: [solution, verification_result] where solution is the step-by-step explanation and verification_result is the GPT verification judgment.

Use only if needed (e.g. new imports).

Args:
    lean_project_path (str, optional): Path to the Lean project. If not provided, it will be inferred from previous tool calls.
    clean (bool, optional): Run `lake clean` before building. Attention: Only use if it is really necessary! It can take a long time! Defaults to False.

Returns:
    str: Build output or error msg

Only use this on INCOMPLETE lines/statements to check available identifiers and imports:
- Dot Completion: Displays relevant identifiers after a dot (e.g., `Nat.`, `x.`, or `Nat.ad`).
- Identifier Completion: Suggests matching identifiers after part of a name.
- Import Completion: Lists importable files after `import` at the beginning of a file.

Args:
    file_path (str): Abs path to Lean file
    line (int): Line number (1-indexed)
    column (int): Column number (1-indexed)
    max_completions (int, optional): Maximum number of completions to return. Defaults to 32

Returns:
    str: List of possible completions or error msg

Note:
    Symbol must be present in the file! Add if necessary!
    Lean files can be large, use `lean_hover_info` before this tool.

Args:
    file_path (str): Abs path to Lean file
    symbol (str): Symbol to look up the declaration for. Case sensitive!

Returns:
    str: File contents or error msg

"no goals to be solved" means code may need removal.

Args:
    file_path (str): Abs path to Lean file

Returns:
    List[str] | str: Diagnostic msgs or error msg

Use sparingly (bloats context). Mainly when unsure about line numbers.

Args:
    file_path (str): Abs path to Lean file
    annotate_lines (bool, optional): Annotate lines with line numbers. Defaults to True.

Returns:
    str: File content or error msg

Highly useful and token-efficient. Slow-ish.

Args:
    file_path (str): Abs path to Lean file

Returns:
    str: Markdown formatted outline or error msg

VERY USEFUL! Main tool to understand the proof state and its evolution!
Returns "no goals" if solved.
To see the goal at sorry, use the cursor before the "s".
Avoid giving a column if unsure-default behavior works well.

Args:
    file_path (str): Abs path to Lean file
    line (int): Line number (1-indexed)
    column (int, optional): Column number (1-indexed). Defaults to None => Both before and after the line.

Returns:
    str: Goal(s) or error msg

Args:
    file_path (str): Abs path to Lean file
    line (int): Line number (1-indexed)
    column (int): Column number (1-indexed)
    num_results (int, optional): Max results. Defaults to 32.

Returns:
    List[str] | str: List of relevant premises or error message

Args:
    file_path (str): Abs path to Lean file
    line (int): Line number (1-indexed)
    column (int): Column number (1-indexed). Make sure to use the start or within the term, not the end.

Returns:
    str: Hover info or error msg

Leandex is a semantic search engine for Lean codebases.
It uses a combination of natural language processing and machine learning to search for theorems and definitions.
It's recommended to use leandex to search whether there exist relevant results before you start to prove a somewhat classic goal.
It's a good practice to query for more general / specific results and then use the results to refine the query if you failed to find the desired results.
You can also use leandex to check the definition of a term or a concept.

Query patterns:
  - Natural language: "If there exist injective maps of sets from A to B and from B to A, then there exists a bijective map between A and B."
  - Mixed natural/Lean: "natural numbers. from: n < m, to: n + 1 < m + 1", "n + 1 <= m if n < m"
  - Concept names: "Cauchy Schwarz"
  - Lean identifiers: "List.sum", "Finset induction"
  - Lean term: "{f : A → B} {g : B → A} (hf : Injective f) (hg : Injective g) : ∃ h, Bijective h"

Args:
    query (str): Search query
    num_results (int, optional): Max results. Defaults to 5.

Returns:
    List[Dict] | str: Search results or error msg

Effective query types:
- Natural language mathematical statement: "For any natural numbers n and m, the sum n+m is equal to m+n."
- Natural language questions: "I'm working with algebraic elements over a field extension … Does this imply that the minimal polynomials of x and y are equal?"
- Proof state. For better results, enter a proof state followed by how you want to transform the proof state.
- Statement definition: Fragment or the whole statement definition.

Tips: Multiple targeted queries beat one complex query.

Args:
    query (str): Mathematical concept or proof state
    num_results (int, optional): Max results. Defaults to 5.

Returns:
    List[Dict] | str: List of Lean statement objects (full name, formal statement, informal statement) or error msg

VERY USEFUL AND FAST!
Pass a short prefix (e.g. ``map_mul``); the metadata shows the declaration kind and file.
The index spans theorems, lemmas, defs, classes, instances, structures, inductives, abbrevs, and opaque decls.

Args:
    query (str): Declaration name or prefix.
    limit (int): Max matches to return (default 10).

Returns:
    List[Dict[str, str]] | str: Matches as ``{"name", "kind", "file"}`` or error message.

Query patterns:
  - By constant: Real.sin  # finds lemmas mentioning Real.sin
  - By lemma name: "differ"  # finds lemmas with "differ" in the name
  - By subexpression: _ * (_ ^ _)  # finds lemmas with a product and power
  - Non-linear: Real.sqrt ?a * Real.sqrt ?a
  - By type shape: (?a -> ?b) -> List ?a -> List ?b
  - By conclusion: |- tsum _ = _ * tsum _
  - By conclusion w/hyps: |- _ < _ → tsum _ < tsum _

Args:
    query (str): Search query
    num_results (int, optional): Max results. Defaults to 8.

Returns:
    List[dict] | str: Search results or error msg

Use to compare tactics or approaches.
Use rarely-prefer direct file edits to keep users involved.
For a single snippet, edit the file and run `lean_diagnostic_messages` instead.

Note:
    Only single-line, fully-indented snippets are supported.
    Avoid comments for best results.

Args:
    file_path (str): Abs path to Lean file
    line (int): Line number (1-indexed)
    snippets (List[str]): List of snippets (3+ are recommended)

Returns:
    List[str] | str: Diagnostics and goal states or error msg

Has to include all imports and definitions!
Only use for testing outside open files! Keep the user in the loop by editing files instead.

Args:
    code (str): Code snippet

Returns:
    List[str] | str: Diagnostics msgs or error msg

Only uses first goal if multiple.

Args:
    file_path (str): Abs path to Lean file
    line (int): Line number (1-indexed)
    column (int): Column number (1-indexed)
    num_results (int, optional): Max results. Defaults to 5.

Returns:
    List | str: Search results or error msg

Args:
    file_path (str): Abs path to Lean file
    line (int): Line number (1-indexed)
    column (int, optional): Column number (1-indexed). Defaults to None => end of line.

Returns:
    str: Expected type or error msg