lean_leanfinder
Read-onlyIdempotent
Search for mathematical theorems and proofs in Lean code using semantic queries based on concepts or proof states to find relevant results.
Instructions
Limit: 10req/30s. Semantic search by mathematical meaning via Lean Finder.
Examples: "commutativity of addition on natural numbers",
"I have h : n < m and need n + 1 < m + 1", proof state text.Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| query | Yes | Mathematical concept or proof state | |
| num_results | No | Max results |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| items | No | List of Lean Finder results |