Semantische Suche über 9 Millionen mathematischer Theoreme
Semantic Search over 9 Million Mathematical Theorems
February 5, 2026
papers.authors: Luke Alexander, Eric Leonen, Sophie Szeto, Artemii Remizov, Ignacio Tejeda, Giovanni Inchiostro, Vasily Ilin
cs.AI
papers.abstract
Die Suche nach mathematischen Ergebnissen bleibt schwierig: Die meisten bestehenden Werkzeuge finden ganze Artikel, während Mathematiker und Theorembeweisagenten oft nach einem spezifischen Theorem, Lemma oder einer Proposition suchen, die eine Anfrage beantwortet. Obwohl semantische Suche rasante Fortschritte gemacht hat, ist ihr Verhalten auf großen, hochtechnischen Korpora wie forschungsnahen mathematischen Theoremen nach wie vor wenig verstanden. In dieser Arbeit führen wir semantische Theorem-Retrieval im großen Maßstab ein und untersuchen es anhand eines vereinheitlichten Korpus von 9,2 Millionen Theoremen, die aus arXiv und sieben weiteren Quellen extrahiert wurden. Dies stellt den größten öffentlich verfügbaren Korpus von menschenverfassten, forschungsnahen Theoremen dar. Wir repräsentieren jedes Theorem durch eine kurze natürliche Beschreibung als Retrieval-Repräsentation und analysieren systematisch, wie Repräsentationskontext, Sprachmodellwahl, Embedding-Modell und Prompting-Strategie die Retrieval-Qualität beeinflussen. Auf einem kuratierten Auswertungsdatensatz von Theorem-Suchanfragen, die von professionellen Mathematikern verfasst wurden, verbessert unser Ansatz sowohl das Theorem- als auch das Paper-Retrieval erheblich im Vergleich zu bestehenden Baseline-Verfahren. Dies zeigt, dass semantische Theorem-Suche auf Web-Skala machbar und effektiv ist. Das Theorem-Suchwerkzeug ist verfügbar unter https://huggingface.co/spaces/uw-math-ai/theorem-search, und der Datensatz ist verfügbar unter 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}.