Recherche sémantique sur plus de 9 millions de théorèmes mathématiques
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
La recherche de résultats mathématiques reste difficile : la plupart des outils existants récupèrent des articles entiers, alors que les mathématiciens et les agents de démonstration de théorèmes cherchent souvent un théorème, lemme ou proposition spécifique répondant à une requête. Si la recherche sémantique a connu des progrès rapides, son comportement sur des corpus volumineux et hautement techniques, comme les théorèmes mathématiques de niveau recherche, reste mal compris. Dans ce travail, nous introduisons et étudions la récupération sémantique de théorèmes à grande échelle sur un corpus unifié de 9,2 millions d'énoncés de théorèmes extraits d'arXiv et de sept autres sources, ce qui représente le plus grand corpus public de théorèmes de niveau recherche rédigés par des humains. Nous représentons chaque théorème par une courte description en langage naturel comme représentation pour la récupération, et nous analysons systématiquement comment le contexte de représentation, le choix du modèle de langage, le modèle d'embedding et la stratégie d'invite affectent la qualité de la récupération. Sur un ensemble d'évaluation de requêtes de recherche de théorèmes rédigées par des mathématiciens professionnels, notre approche améliore considérablement la récupération au niveau du théorème et au niveau de l'article par rapport aux bases de référence existantes, démontrant que la recherche sémantique de théorèmes est réalisable et efficace à l'échelle du web. L'outil de recherche de théorèmes est disponible à l'adresse https://huggingface.co/spaces/uw-math-ai/theorem-search, et le jeu de données est disponible à l'adresse 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}.