Lean LSP MCP

Overview Schema Source Related Servers Discussions Admin

lean_minimal_hypotheses

Destructive

Identifies which explicit theorem hypotheses are load-bearing by dropping each one and re-elaborating a scratch copy, reporting unused binders without editing the file.

Instructions

For each explicit (h : T) hypothesis of a theorem, drop it and re-elaborate a scratch copy of the file. Reports which hypotheses are load-bearing and which are actually unused. Skips implicit {x : α} and instance [inst : C] binders (those are usually inferable / always load-bearing). Does not rewrite the proof body — a body that names h will fail to elaborate without the binder, which is the truthful answer (load-bearing).

Variants are checked in parallel on scratch documents; the file is never edited.

Tool call template

Replace each placeholder with a value matching the input schema. Only required parameters are included; add optional parameters as needed.

{
  "id": 1,
  "jsonrpc": "2.0",
  "method": "tools/call",
  "params": {
    "arguments": {
      "file_path": "<file_path>",
      "theorem_name": "<theorem_name>"
    },
    "name": "lean_minimal_hypotheses"
  }
}

Input Schema

Name	Required	Description
`file_path`	Yes	Absolute path to Lean file
`theorem_name`	Yes	Theorem name. Either bare (e.g. `add_comm`) or fully qualified (e.g. `Namespace.add_comm`); only the trailing segment is used for source matching.
`inactivity_timeout`	No	Per-hypothesis elaboration timeout (seconds)

Output Schema

Name	Required	Description
`file`	Yes	Relative file path
`verdicts`	No	One verdict per explicit (h : T) binder, in source order
`theorem_name`	Yes	Theorem analyzed
`skipped_implicit`	No	Count of implicit {x : α} / instance [inst] binders not probed

Schema Changelog

Changes observed during successful MCP inspections.

Changed3 schema fields changedv0.31.0Oct 3, 2026

addedOutput schema / $defs / DiagnosticCategory

Added value: +{
+  "enum": [
+    "diagnostic",
+    "linter",
+    "sorry",
+    "suggestion"
+  ],
+  "title": "DiagnosticCategory",
+  "type": "string"
+}

addedOutput schema / $defs / DiagnosticMessage / properties / category

Added value: +{
+  "$ref": "#/$defs/DiagnosticCategory",
+  "default": "diagnostic",
+  "description": "'linter' is style noise (unused variables and the like) that does not block compilation; 'sorry' marks an unproved declaration and is never noise; 'suggestion' carries a `Try this:` replacement; 'diagnostic' is everything else."
+}

addedOutput schema / $defs / DiagnosticMessage / properties / hint

Added value: +{
+  "anyOf": [
+    {
+      "type": "string"
+    },
+    {
+      "type": "null"
+    }
+  ],
+  "default": null,
+  "description": "Guidance for a recognised failure mode, when one applies",
+  "title": "Hint"
+}

Addedv0.28.0Jul 11, 2026

TDQS

A4.2/5.0

Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

Adds substantial behavior beyond annotations: work happens on scratch copies in parallel, the target file is never edited, and the proof body is not rewritten, so elaboration failure is reported as load-bearing rather than patched. There is mild tension with `destructiveHint: true` / `readOnlyHint: false`, which the description does not explain (likely scratch-document creation/teardown), but the description does not deny a write — it scopes it to the source file.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Front-loaded with the core action, then the skip rules, then the non-rewriting semantics, then the parallelism guarantee. Each of the four sentences carries distinct information and nothing is redundant.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

An output schema exists, so return-value shape need not be described, and the description covers the non-obvious semantics an agent needs: skip rules, failure interpretation, and non-mutation of the file. Only the mismatch between the stated no-edit behavior and the destructive annotation is left unexplained.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema coverage is 100%, so `file_path`, `theorem_name` (bare vs qualified, trailing-segment matching), and `inactivity_timeout` are already documented. The description adds no parameter-level detail of its own; its 'explicit hypothesis' scoping is about what gets tested, not about any input field.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

States a precise verb+resource pair: for each explicit `(h : T)` hypothesis, drop it and re-elaborate a scratch copy, reporting load-bearing vs unused. No sibling (`lean_multi_attempt`, `lean_verify`, `lean_goal`) does hypothesis minimization, and the scoping to explicit binders makes the tool unmistakable.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Gives clear selection context: it only touches explicit `(h : T)` hypotheses and deliberately skips implicit `{x : α}` and instance `[inst : C]` binders, with a rationale. It stops short of naming an alternative tool or stating when not to use it at all (e.g., for theorems with no explicit hypotheses).

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.