Ricerca Semantica su oltre 9 Milioni di Teoremi Matematici
Semantic Search over 9 Million Mathematical Theorems
February 5, 2026
Autori: Luke Alexander, Eric Leonen, Sophie Szeto, Artemii Remizov, Ignacio Tejeda, Giovanni Inchiostro, Vasily Ilin
cs.AI
Abstract
La ricerca di risultati matematici rimane difficile: la maggior parte degli strumenti esistenti recupera interi articoli, mentre matematici e agenti di dimostrazione di teoremi spesso cercano un teorema, lemma o proposizione specifico che risponda a una query. Sebbene la ricerca semantica abbia fatto rapidi progressi, il suo comportamento su corpora ampi e altamente tecnici, come i teoremi matematici di livello di ricerca, rimane poco compreso. In questo lavoro, introduciamo e studiamo il recupero semantico di teoremi su larga scala su un corpus unificato di 9,2 milioni di enunciati di teoremi estratti da arXiv e da altre sette fonti, che rappresenta il più grande corpus pubblicamente disponibile di teoremi di livello di ricerca creati da esseri umani. Rappresentiamo ogni teorema con una breve descrizione in linguaggio naturale come rappresentazione per il recupero e analizziamo sistematicamente come il contesto della rappresentazione, la scelta del modello linguistico, il modello di embedding e la strategia di prompting influenzino la qualità del recupero. Su un set di valutazione curato di query di ricerca di teoremi scritte da matematici professionisti, il nostro approccio migliora sostanzialmente sia il recupero a livello di teorema che a livello di articolo rispetto ai baseline esistenti, dimostrando che la ricerca semantica di teoremi è fattibile ed efficace su scala web. Lo strumento di ricerca di teoremi è disponibile all'indirizzo https://huggingface.co/spaces/uw-math-ai/theorem-search, e il dataset è disponibile all'indirizzo https://huggingface.co/datasets/uw-math-ai/TheoremSearch.
English
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 theorem search tool is available at https://huggingface.co/spaces/uw-math-ai/theorem-search{this link}, and the dataset is available at https://huggingface.co/datasets/uw-math-ai/TheoremSearch{this link}.