Saved in:
| Main Authors: | , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2602.05216 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915841507852288 |
|---|---|
| author | Alexander, Luke Leonen, Eric Szeto, Sophie Remizov, Artemii Tejeda, Ignacio Alper, Jarod Inchiostro, Giovanni Ilin, Vasily |
| author_facet | Alexander, Luke Leonen, Eric Szeto, Sophie Remizov, Artemii Tejeda, Ignacio Alper, Jarod Inchiostro, Giovanni Ilin, Vasily |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2602_05216 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Semantic Search over 9 Million Mathematical Theorems Alexander, Luke Leonen, Eric Szeto, Sophie Remizov, Artemii Tejeda, Ignacio Alper, Jarod Inchiostro, Giovanni Ilin, Vasily Information Retrieval Artificial Intelligence History and Overview 68P20 (primary) 68T50, 01A99 (secondary) H.3.3; I.2.7; H.3.1 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. |
| title | Semantic Search over 9 Million Mathematical Theorems |
| topic | Information Retrieval Artificial Intelligence History and Overview 68P20 (primary) 68T50, 01A99 (secondary) H.3.3; I.2.7; H.3.1 |
| url | https://arxiv.org/abs/2602.05216 |