lean_multi_attempt
Read-onlyIdempotent
Test multiple tactics in Lean theorem prover without modifying files. Returns goal state results for each tactic to help identify effective proof strategies.
Instructions
Try multiple tactics without modifying file. Returns goal state for each.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | Absolute path to Lean file | |
| line | Yes | Line number (1-indexed) | |
| snippets | Yes | Tactics to try (3+ recommended) |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| items | No | List of attempt results |