lean_leandex
Search Lean codebases semantically for theorems and definitions using natural language or Lean terms, helping you check if a result already exists before proving it.
Instructions
Search for theorems and definitions using leandex.
Leandex is a semantic search engine for Lean codebases.
It uses a combination of natural language processing and machine learning to search for theorems and definitions.
It's recommended to use leandex to search whether there exist relevant results before you start to prove a somewhat classic goal.
It's a good practice to query for more general / specific results and then use the results to refine the query if you failed to find the desired results.
You can also use leandex to check the definition of a term or a concept.
Query patterns:
- Natural language: "If there exist injective maps of sets from A to B and from B to A, then there exists a bijective map between A and B."
- Mixed natural/Lean: "natural numbers. from: n < m, to: n + 1 < m + 1", "n + 1 <= m if n < m"
- Concept names: "Cauchy Schwarz"
- Lean identifiers: "List.sum", "Finset induction"
- Lean term: "{f : A → B} {g : B → A} (hf : Injective f) (hg : Injective g) : ∃ h, Bijective h"
Args:
query (str): Search query
num_results (int, optional): Max results. Defaults to 5.
Returns:
List[Dict] | str: Search results 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 |