Semantisch Zoeken in Meer dan 9 Miljoen Wiskundige Stellingen
Semantic Search over 9 Million Mathematical Theorems
February 5, 2026
Auteurs: Luke Alexander, Eric Leonen, Sophie Szeto, Artemii Remizov, Ignacio Tejeda, Giovanni Inchiostro, Vasily Ilin
cs.AI
Samenvatting
Het zoeken naar wiskundige resultaten blijft moeilijk: de meeste bestaande tools halen volledige artikelen op, terwijl wiskundigen en bewijsassistenten vaak op zoek zijn naar een specifieke stelling, lemma of propositie die een vraag beantwoordt. Hoewel semantisch zoeken een snelle vooruitgang heeft doorgemaakt, is het gedrag ervan op grote, zeer technische corpora zoals wiskundige stellingen op onderzoeksniveau nog steeds slecht begrepen. In dit werk introduceren en bestuderen we semantische stellingenretrieval op grote schaal over een verenigd corpus van 9,2 miljoen stellingen die zijn geëxtraheerd uit arXiv en zeven andere bronnen, wat het grootste openbaar beschikbare corpus van door mensen geschreven stellingen op onderzoeksniveau vertegenwoordigt. We vertegenwoordigen elke stelling met een korte beschrijving in natuurlijke taal als een retrievoorstelling en analyseren systematisch hoe de context van de voorstelling, de keuze van het taalmodel, het embeddingmodel en de promptingstrategie de retrievakwaliteit beïnvloeden. Op een samengestelde evaluatieset van zoekopdrachten voor stellingen, geschreven door professionele wiskundigen, verbetert onze aanpak zowel de retrieval op stellingsniveau als op artikelniveau aanzienlijk in vergelijking met bestaande baseline-methoden, wat aantoont dat semantisch zoeken naar stellingen haalbaar en effectief is op webschaal. De zoektool voor stellingen is beschikbaar op https://huggingface.co/spaces/uw-math-ai/theorem-search, en de dataset is beschikbaar op 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}.