lean_leanfinder
Search Mathlib theorems and definitions semantically by mathematical concept, proof state, or statement fragment to locate relevant Lean statements.
Instructions
Limit: 10req/30s. Search Mathlib theorems/definitions semantically by mathematical concept or proof state using Lean Finder.
Effective query types:
- Natural language mathematical statement: "For any natural numbers n and m, the sum n+m is equal to m+n."
- Natural language questions: "I'm working with algebraic elements over a field extension … Does this imply that the minimal polynomials of x and y are equal?"
- Proof state. For better results, enter a proof state followed by how you want to transform the proof state.
- Statement definition: Fragment or the whole statement definition.
Tips: Multiple targeted queries beat one complex query.
Args:
query (str): Mathematical concept or proof state
num_results (int, optional): Max results. Defaults to 5.
Returns:
List[Dict] | str: List of Lean statement objects (full name, formal statement, informal statement) or error msg
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| query | Yes | ||
| num_results | No |
Output Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| result | Yes |