lean_loogle
Search Mathlib theorems by type signature or name to find relevant mathematical proofs and definitions for Lean theorem proving.
Instructions
Search Mathlib by type signature via loogle.lean-lang.org.
Examples: `Real.sin`, `"comm"`, `(?a → ?b) → List ?a → List ?b`,
`_ * (_ ^ _)`, `|- _ < _ → _ + 1 < _ + 1`
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| query | Yes | Type pattern, constant, or name substring | |
| num_results | No | Max results |