Semantic Mathlib search

Describe the result you need.

Search 310,579 declarations by meaning, plus 10,000 selected theorems with exact statements and source links from a separate pinned Mathlib revision.

the order of a group element divides the order of the group continuous function on a compact set is bounded Cauchy Schwarz inequality for finite sums prime divides a product

Search the published corpus

Natural-language retrieval covers the complete LeanSearch v2 Mathlib declaration dataset, including theorem statements, definitions, names, modules, and generated descriptions.

Need exact Lean structure?

Use Lean shapes for wildcards, metavariables, conclusion filters, and genuine elaborated matching through Loogle.

Search Lean shapes