| lean_buildA | Build the Lean project and restart the LSP Server. 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
|
| lean_file_contentsA | DEPRECATED: Will be removed soon. Get the text contents of a Lean file, optionally with line numbers. 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
|
| lean_file_outlineA | Get a concise outline showing imports and declarations with type signatures (theorems, defs, classes, structures). Highly useful and token-efficient. Slow-ish.
Args:
file_path (str): Abs path to Lean file
Returns:
str: Markdown formatted outline or error msg
|
| lean_diagnostic_messagesA | Get all diagnostic msgs (errors, warnings, infos) for a Lean file. "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
|
| lean_goalA | Get the proof goals (proof state) at a specific location in a Lean file. 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
|
| lean_term_goalA | Get the expected type (term goal) at a specific location in a Lean file. 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
|
| lean_hover_infoA | Get hover info (docs for syntax, variables, functions, etc.) at a specific location in a Lean file. 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
|
| lean_completionsA | Get code completions at a location in a Lean file. 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
|
| lean_declaration_fileA | Get the file contents where a symbol/lemma/class/structure is declared. 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
|
| lean_multi_attemptA | Try multiple Lean code snippets at a line and get the goal state and diagnostics for each. 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
|
| lean_run_codeA | Run a complete, self-contained code snippet and return diagnostics. 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
|
| lean_local_searchA | Confirm declarations exist in the current workspace to prevent hallucinating APIs. 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.
|
| lean_leandexA | Search for theorems and definitions using leandex. 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
|
| lean_loogleA | Limit: 3req/30s. Search for definitions and theorems using loogle. 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
|
| lean_leanfinderA | Limit: 10req/30s. Search Mathlib theorems/definitions semantically by mathematical concept or proof state using Lean Finder. 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
|
| lean_state_searchA | Limit: 3req/30s. Search for theorems based on proof state using premise-search.com. 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
|
| lean_hammer_premiseA | Limit: 3req/30s. Search for premises based on proof state using the lean hammer premise search. 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
|
| gemini_code_golfC | This tool uses the Google Gemini model to simplify Lean code compiled by the compiler. 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
|
| gemini_informal_proverA | 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.
|
| gpt_informal_proverB | 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.
|
| discussion_partnerA | Use this tool to interact with a specialized partner model for proof strategies, reasoning, and formalization. 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.
|
