lean_state_search
Find relevant lemmas to close goals in Lean theorem prover files by searching premise-search.com for mathematical proofs at specific positions.
Instructions
Limit: 3req/30s. Find lemmas to close the goal at a position. Searches premise-search.com.
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | Absolute path to Lean file | |
| line | Yes | Line number (1-indexed) | |
| column | Yes | Column number (1-indexed) | |
| num_results | No | Max results |