lean_leansearch
Search Mathlib theorems using natural language queries to find mathematical proofs and definitions in Lean code.
Instructions
Limit: 3req/30s. Search Mathlib via leansearch.net using natural language.
Examples: "sum of two even numbers is even", "Cauchy-Schwarz inequality",
"{f : A → B} (hf : Injective f) : ∃ g, LeftInverse g f"
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| query | Yes | Natural language or Lean term query | |
| num_results | No | Max results |