# A Semantic Search Engine for Mathlib4

arXiv: https://arxiv.org/abs/2403.13310 · HTML: https://mlsanity.com/paper/2403.13310/

## Key facts

- Cited by 31 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 42 references that are in the map.
- First posted on arXiv 20 Mar 2024.

## Builds on (most cited first, 20 of 20)

- [Dense Passage Retrieval for Open-Domain Question Answering](https://mlsanity.com/paper/2004.04906/) (2020)
- [Text Embeddings by Weakly-Supervised Contrastive Pre-training](https://mlsanity.com/paper/2212.03533/) (2022)
- [ColBERT: Efficient and Effective Passage Search via Contextualized Late Interaction over BERT](https://mlsanity.com/paper/2004.12832/) (2020)
- [Efficient and robust approximate nearest neighbor search using Hierarchical Navigable Small World graphs](https://mlsanity.com/paper/1603.09320/) (2016)
- [Latent Retrieval for Weakly Supervised Open Domain Question Answering](https://mlsanity.com/paper/1906.00300/) (2019)
- [Sentence-T5: Scalable Sentence Encoders from Pre-trained Text-to-Text Models](https://mlsanity.com/paper/2108.08877/) (2021)
- [Large Dual Encoders Are Generalizable Retrievers](https://mlsanity.com/paper/2112.07899/) (2021)
- [RocketQA: An Optimized Training Approach to Dense Passage Retrieval for Open-Domain Question Answering](https://mlsanity.com/paper/2010.08191/) (2020)
- [Document Ranking with a Pretrained Sequence-to-Sequence Model](https://mlsanity.com/paper/2003.06713/) (2020)
- [Text and Code Embeddings by Contrastive Pre-Training](https://mlsanity.com/paper/2201.10005/) (2022)
- [One Embedder, Any Task: Instruction-Finetuned Text Embeddings](https://mlsanity.com/paper/2212.09741/) (2022)
- [Improving Text Embeddings with Large Language Models](https://mlsanity.com/paper/2401.00368/) (2023)
- [Pre-training Tasks for Embedding-based Large-scale Retrieval](https://mlsanity.com/paper/2002.03932/) (2020)
- [AnglE-optimized Text Embeddings](https://mlsanity.com/paper/2309.12871/) (2023)
- [End-to-End Neural Ad-hoc Ranking with Kernel Pooling](https://mlsanity.com/paper/1706.06613/) (2017)
- [Understanding the Behaviors of BERT in Ranking](https://mlsanity.com/paper/1904.07531/) (2019)
- [Multilingual Mathematical Autoformalization](https://mlsanity.com/paper/2311.03755/) (2023)
- [Entity-Duet Neural Ranking: Understanding the Role of Knowledge Graph Semantics in Neural Information Retrieval](https://mlsanity.com/paper/1805.07591/) (2018)
- [Deep Relevance Ranking Using Enhanced Document-Query Interactions](https://mlsanity.com/paper/1809.01682/) (2018)
- [Evaluating Token-Level and Passage-Level Dense Retrieval Models for Math Information Retrieval](https://mlsanity.com/paper/2203.11163/) (2022)

## Built on by (most cited first, 30 of 31)

- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [Automated Conjecture Resolution with Formal Verification](https://mlsanity.com/paper/2604.03789/) (2026)
- [Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graph](https://mlsanity.com/paper/2510.04520/) (2025)
- [REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoning](https://mlsanity.com/paper/2505.20613/) (2025)
- [LeanExplore: A search engine for Lean 4 declarations](https://mlsanity.com/paper/2506.11085/) (2025)
- [ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddings](https://mlsanity.com/paper/2510.15681/) (2025)
- [A Minimal Agent for Automated Theorem Proving](https://mlsanity.com/paper/2602.24273/) (2026)
- [LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks](https://mlsanity.com/paper/2606.03303/) (2026)
- [LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Proving](https://mlsanity.com/paper/2605.13137/) (2026)
- [Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization](https://mlsanity.com/paper/2606.31002/) (2026)
- [DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theorems](https://mlsanity.com/paper/2510.10815/) (2025)
- [Lean Finder: Semantic Search for Mathlib That Understands User Intents](https://mlsanity.com/paper/2510.15940/) (2025)
- [Semantic Search over 9 Million Mathematical Theorems](https://mlsanity.com/paper/2602.05216/) (2026)
- [SorryDB: Can AI Provers Complete Real-World Lean Theorems?](https://mlsanity.com/paper/2603.02668/) (2026)
- [MIRB: Mathematical Information Retrieval Benchmark](https://mlsanity.com/paper/2505.15585/) (2025)
- [Automated Formalization via Conceptual Retrieval-Augmented LLMs](https://mlsanity.com/paper/2508.06931/) (2025)
- [DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agent](https://mlsanity.com/paper/2604.26311/) (2026)
- [TheoremGraph: Bridging Formal and Informal Mathematics](https://mlsanity.com/paper/2606.25363/) (2026)
- [Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalization](https://mlsanity.com/paper/2501.13959/) (2025)
- [MathAtlas: A Benchmark for Autoformalization in the Wild](https://mlsanity.com/paper/2605.14061/) (2026)
- [Matlas: A Semantic Search Engine for Mathematics](https://mlsanity.com/paper/2604.17484/) (2026)
- [COMPOSE: Composing Future Theorems from Citations and Formal Structure](https://mlsanity.com/paper/2605.30333/) (2026)
- [Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifacts](https://mlsanity.com/paper/2606.03743/) (2026)
- [TheoremForge: Scaling up Formal Data Synthesis with Low-Budget Agentic Workflow](https://mlsanity.com/paper/2601.17332/) (2026)
- [SABER-Math: Automated Benchmark for Information Retrieval Evaluation in Mathematics](https://mlsanity.com/paper/2606.29894/) (2026)
- [Awakening the Sleeping Agent: Lean-Specific Agentic Data Reactivates General Tool Use in Goedel Prover](https://mlsanity.com/paper/2604.08388/) (2026)
- [Re2Math: Benchmarking Theorem Retrieval in Research-Level Mathematics](https://mlsanity.com/paper/2605.09012/) (2026)
- [Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalization](https://mlsanity.com/paper/2609.39228/) (2026)

## Abstract (arXiv)

The interactive theorem prover Lean enables the verification of formal mathematical proofs and is backed by an expanding community. Central to this ecosystem is its mathematical library, mathlib4, which lays the groundwork for the formalization of an expanding range of mathematical theories. However, searching for theorems in mathlib4 can be challenging. To successfully search in mathlib4, users often need to be familiar with its naming conventions or documentation strings. Therefore, creating a semantic search engine that can be used easily by individuals with varying familiarity with mathlib4 is very important. In this paper, we present a semantic search engine (https://leansearch.net/) for mathlib4 that accepts informal queries and finds the relevant theorems. We also establish a benchmark for assessing the performance of various search engines for mathlib4.