mlsanityData to 7 Oct 2026

A Semantic Search Engine for Mathlib4

arXiv 2403.13310 ↗First posted 20 Mar 2024cs.IR cs.LG cs.LOcited by 30

Not on the map. Why?

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.

Key facts. Cited by 30 papers in the map (data through 7 Oct 2026). Builds on 20 of its 42 references that are in the map. First posted on arXiv 20 Mar 2024.

Builds on

20 of 42 references.

References · 20

  1. 2020Dense Passage Retrieval for Open-Domain Question Answeringcited by 3,779
  2. 2022Text Embeddings by Weakly-Supervised Contrastive Pre-trainingcited by 1,216
  3. 2020ColBERT: Efficient and Effective Passage Search via Contextualized Late Interaction over BERTcited by 1,160
  4. 2016Efficient and robust approximate nearest neighbor search using Hierarchical Navigable Small World graphscited by 853
  5. 2019Latent Retrieval for Weakly Supervised Open Domain Question Answeringcited by 691
  6. 2021Sentence-T5: Scalable Sentence Encoders from Pre-trained Text-to-Text Modelscited by 462
  7. 2021Large Dual Encoders Are Generalizable Retrieverscited by 454
  8. 2020RocketQA: An Optimized Training Approach to Dense Passage Retrieval for Open-Domain Question Answeringcited by 410
  9. 2020Document Ranking with a Pretrained Sequence-to-Sequence Modelcited by 373
  10. 2022Text and Code Embeddings by Contrastive Pre-Trainingcited by 358
  11. 2022One Embedder, Any Task: Instruction-Finetuned Text Embeddingscited by 329
  12. 2023Improving Text Embeddings with Large Language Modelscited by 295
8 more
  1. 2020Pre-training Tasks for Embedding-based Large-scale Retrievalcited by 153
  2. 2023AnglE-optimized Text Embeddingscited by 98
  3. 2017End-to-End Neural Ad-hoc Ranking with Kernel Poolingcited by 85
  4. 2019Understanding the Behaviors of BERT in Rankingcited by 49
  5. 2023Multilingual Mathematical Autoformalizationcited by 38
  6. 2018Entity-Duet Neural Ranking: Understanding the Role of Knowledge Graph Semantics in Neural Information Retrievalcited by 33
  7. 2018Deep Relevance Ranking Using Enhanced Document-Query Interactionscited by 13
  8. 2022Evaluating Token-Level and Passage-Level Dense Retrieval Models for Math Information Retrievalcited by 9

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 1; 2025: 11; 2026: 18.

30 papers.

Sort:

By area:

  1. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  2. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  3. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 55
  4. 2026Automated Conjecture Resolution with Formal Verificationcited by 21
  5. 2025REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoningcited by 18
  6. 2025Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graphcited by 18
  7. 2025ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddingscited by 16
  8. 2025LeanExplore: A search engine for Lean 4 declarationscited by 13
  9. 2026A Minimal Agent for Automated Theorem Provingcited by 13
  10. 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworkscited by 11
  11. 2025DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theoremscited by 8
  12. 2025Lean Finder: Semantic Search for Mathlib That Understands User Intentscited by 7
18 more
  1. 2026Semantic Search over 9 Million Mathematical Theoremscited by 7
  2. 2026LeanSearch v2: Global Premise Retrieval for Lean 4 Theorem Provingcited by 7
  3. 2025MIRB: Mathematical Information Retrieval Benchmarkcited by 5
  4. 2025Automated Formalization via Conceptual Retrieval-Augmented LLMscited by 5
  5. 2025Learning an Effective Premise Retrieval Model for Efficient Mathematical Formalizationcited by 4
  6. 2026SorryDB: Can AI Provers Complete Real-World Lean Theorems?cited by 4
  7. 2026DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agentcited by 4
  8. 2026TheoremGraph: Bridging Formal and Informal Mathematicscited by 4
  9. 2026Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalizationcited by 4
  10. 2026Matlas: A Semantic Search Engine for Mathematicscited by 3
  11. 2026MathAtlas: A Benchmark for Autoformalization in the Wildcited by 2
  12. 2026COMPOSE: Composing Future Theorems from Citations and Formal Structurecited by 2
  13. 2026Proof-Refactor: Refactoring Generated Formal Proofs into Modular Artifactscited by 2
  14. 2026TheoremForge: Scaling up Formal Data Synthesis with Low-Budget Agentic Workflowcited by 1
  15. 2026Awakening the Sleeping Agent: Lean-Specific Agentic Data Reactivates General Tool Use in Goedel Provercited by 0
  16. 2026Re2Math: Benchmarking Theorem Retrieval in Research-Level Mathematicscited by 0
  17. 2026SABER-Math: Automated Benchmark for Information Retrieval Evaluation in Mathematicscited by 0
  18. 2026Fyan: A Human--AI Harness with Semantic Auditing for Document-Level Formalizationcited by 0