# Semantic Search over 9 Million Mathematical Theorems

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 56 references that are in the map.
- First posted on arXiv 5 Feb 2026.

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

- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks](https://mlsanity.com/paper/2005.11401/) (2020)
- [Sentence-BERT: Sentence Embeddings using Siamese BERT-Networks](https://mlsanity.com/paper/1908.10084/) (2019)
- [Dense Passage Retrieval for Open-Domain Question Answering](https://mlsanity.com/paper/2004.04906/) (2020)
- [Datasheets for Datasets](https://mlsanity.com/paper/1803.09010/) (2018)
- [Qwen3 Embedding: Advancing Text Embedding and Reranking Through Foundation Models](https://mlsanity.com/paper/2506.05176/) (2025)
- [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)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Multilingual E5 Text Embeddings: A Technical Report](https://mlsanity.com/paper/2402.05672/) (2024)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [EmbeddingGemma: Powerful and Lightweight Text Representations](https://mlsanity.com/paper/2509.20354/) (2025)
- [MathBERT: A Pre-Trained Model for Mathematical Formula Understanding](https://mlsanity.com/paper/2105.00377/) (2021)
- [Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics](https://mlsanity.com/paper/2601.14027/) (2026)
- [Multilingual Mathematical Autoformalization](https://mlsanity.com/paper/2311.03755/) (2023)
- [KaLM-Embedding: Superior Training Data Brings A Stronger Embedding Model](https://mlsanity.com/paper/2501.01028/) (2025)
- [A Semantic Search Engine for Mathlib4](https://mlsanity.com/paper/2403.13310/) (2024)
- [LeanExplore: A search engine for Lean 4 declarations](https://mlsanity.com/paper/2506.11085/) (2025)
- [WithdrarXiv: A Large-Scale Dataset for Retraction Study](https://mlsanity.com/paper/2412.03775/) (2024)
- [Homotopy Type Theory: Univalent Foundations of Mathematics](https://mlsanity.com/paper/1308.0729/) (2013)
- [Evaluating NLP Embedding Models for Handling Science-Specific Symbolic Expressions in Student Texts](https://mlsanity.com/paper/2505.17950/) (2025)

## Built on by (most cited first, 8 of 8)

- [LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematics](https://mlsanity.com/paper/2602.24173/) (2026)
- [TheoremGraph: Bridging Formal and Informal Mathematics](https://mlsanity.com/paper/2606.25363/) (2026)
- [Albilich: Steerable Proof-State Orchestration for LLM-Based Mathematical Research with CAS Integration](https://mlsanity.com/paper/2607.27705/) (2026)
- [Matlas: A Semantic Search Engine for Mathematics](https://mlsanity.com/paper/2604.17484/) (2026)
- [Does My Embedding Reflect That A = B? Evaluating Mathematical Equivalence in Embedding Models](https://mlsanity.com/paper/2606.23959/) (2026)
- [RL-Index: Reinforcement Learning for Retrieval Index Reasoning](https://mlsanity.com/paper/2606.16316/) (2026)
- [Lean Pool: An AI-Maintained Archive of Formalized Mathematics](https://mlsanity.com/paper/2609.25199/) (2026)
- [Beyond Correctness: Toward Automated Novelty Verification with Lean 4](https://mlsanity.com/paper/2608.14669/) (2026)

## Abstract (arXiv)

Searching for mathematical results remains difficult: most existing tools retrieve entire papers, while mathematicians and theorem-proving agents often seek a specific theorem, lemma, or proposition that answers a query. While semantic search has seen rapid progress, its behavior on large, highly technical corpora such as research-level mathematical theorems remains poorly understood. In this work, we introduce and study semantic theorem retrieval at scale over a unified corpus of 9.2 million theorem statements extracted from arXiv and seven other sources, representing the largest publicly available corpus of human-authored, research-level theorems. We represent each theorem with a short natural-language description as a retrieval representation and systematically analyze how representation context, language model choice, embedding model, and prompting strategy affect retrieval quality. On a curated evaluation set of theorem-search queries written by professional mathematicians, our approach substantially improves both theorem-level and paper-level retrieval compared to existing baselines, demonstrating that semantic theorem search is feasible and effective at web scale. The project page, search tool, dataset, REST API, and MCP server are available at theoremsearch.com.