Lean Finder: Semantic Search for Mathlib That Understands User Intents
Lean Finder is an advanced AI-powered semantic search engine designed specifically for
Lean 4 and mathlib.
Unlike traditional search tools, Lean Finder understands the diverse intents and contexts behind
mathematicians' queries, achieving an 81.6% user preference rate compared to 56.9% for existing tools.
Key Performance: Over 30% improvement in retrieval accuracy | 1.4M+ query-code pairs |
Supports 230k+ theorems from mathlib4
Supported Query Types
1. Informalized Statement
Enter an informal translation of a formal Lean statement, and find relevant Lean statements.
Perfect for mathematicians who think in natural language but need formal proofs.
2. User Question
Ask any question about Lean statements. Whether you're searching for existing lemmas,
exploring type-class instances, or seeking proof engineering guidance, Lean Finder
understands your intent and provides relevant formal mathematics.
3. Proof State
Enter the proof state of a theorem. For better results, enter a proof state followed
by how you want to transform the proof state. This augmented approach helps identify
the most relevant tactics and lemmas for your specific proof context.
4. Statement Definition
Enter any fragment or the whole statement definition, and find statements that match
the entered content. Note that the query syntax doesn't need to be perfect - Lean Finder
is robust to variations and partial matches.
Why Choose Lean Finder?
Traditional Lean search engines focus on surface-level matching between informal and formal statements.
Lean Finder goes beyond by understanding the intent behind your queries. Whether you're:
- Searching for existing code or lemmas in mathlib
- Working with metaprogramming and tactics
- Resolving type-class or instance issues
- Engineering proofs for everyday Lean usage
- Designing libraries for large-scale formalization
Lean Finder provides contextually relevant results that accelerate your formal mathematics workflow.
Ready to experience better Lean search?
Try Lean Finder now →
Lean Finder semantic search mathlib4 Lean 4 theorem prover formal mathematics proof assistant
mathematical search engine natural language processing NLP AI retrieval augmented generation
formal verification automated theorem proving interactive theorem prover dependent type theory
Lean programming language functional programming formal methods mathematical logic
proof engineering tactics metaprogramming type classes instances formal statements
informal mathematics autoformalization proof states lemma search theorem search
mathematical retrieval system semantic embedding vector search mathematical AI