Lean LSP MCP

Overview Schema Source Related Servers Discussions Admin

lean_minimal_hypotheses

Read-onlyIdempotent

Find which explicit hypotheses in a Lean theorem are load-bearing or unused by dropping each in a scratch re-elaboration.

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.

Input Schema

TableJSON 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

TableJSON 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

Behavior5/5

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

Annotations already convey readOnly/idempotent/closed-world safety, but the description adds meaningful behavior: the file is never edited, variants run in parallel on scratch documents, and a body naming `h` failing to elaborate is the intended truthful signal. The 'does not rewrite the proof body' caveat is exactly the kind of context annotations cannot express.

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

Conciseness4/5

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

Front-loaded with the core operation, followed by scope exclusions and behavioral notes. Every sentence contributes, though the explanation of why a failing body is 'the truthful answer' is slightly verbose for the value it adds.

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

Completeness5/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 values need not be described, and the description still summarizes the report ('which hypotheses are load-bearing'). With annotations covering the safety profile and full schema coverage, nothing essential for correct invocation is missing.

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 description coverage is 100%, so file_path, theorem_name, and inactivity_timeout are already fully documented in the schema. The description adds no parameter-level detail beyond that, so the baseline 3 is appropriate.

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 specific operation on a specific resource: drop each explicit `(h : T)` hypothesis and re-elaborate a scratch copy to report load-bearing vs unused hypotheses. This is a distinctive purpose that no sibling tool shares, so an agent can identify it without ambiguity.

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

Usage Guidelines3/5

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

The description clarifies scope (only explicit binders; implicit/instance binders are skipped and why), which is real selection guidance. However, it never states when to reach for this tool versus alternatives such as lean_verify or lean_multi_attempt, so the usage framing is implied rather than explicit.

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