lean_minimal_hypotheses
Read-onlyIdempotent
Tests each explicit hypothesis of a Lean theorem to determine if it is load-bearing or unused, by re-elaborating the proof without it. Skips implicit and instance binders.
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 | Default |
|---|---|---|---|
| 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 | Default |
|---|---|---|---|
| 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 |