lean_leanfinder
Search for mathematical theorems and proofs in Lean code using semantic meaning. Enter 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 |