{"id":"arxiv/2602.05216","url":"https://arxiv.org/abs/2602.05216","tags":["cs.IR","cs.AI","math.HO"],"score":0,"title":"Semantic Search over 9 Million Mathematical Theorems","domain":"cs.IR","source":"arxiv","authors":["Luke Alexander","Eric Leonen","Sophie Szeto","Artemii Remizov","Ignacio Tejeda","Jarod Alper","Giovanni Inchiostro","Vasily Ilin"],"reviews":0,"subject":"cs.IR","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-02-05","reactions":{}}