Búsqueda Semántica sobre 9 Millones de Teoremas Matemáticos
Semantic Search over 9 Million Mathematical Theorems
February 5, 2026
Autores: Luke Alexander, Eric Leonen, Sophie Szeto, Artemii Remizov, Ignacio Tejeda, Giovanni Inchiostro, Vasily Ilin
cs.AI
Resumen
La búsqueda de resultados matemáticos sigue siendo difícil: la mayoría de las herramientas existentes recuperan artículos completos, mientras que los matemáticos y los agentes de demostración de teoremas a menudo buscan un teorema, lema o proposición específico que responda a una consulta. Si bien la búsqueda semántica ha experimentado un rápido progreso, su comportamiento en corpus grandes y altamente técnicos, como los teoremas matemáticos de nivel de investigación, sigue siendo poco conocido. En este trabajo, introducimos y estudiamos la recuperación semántica de teoremas a gran escala sobre un corpus unificado de 9,2 millones de enunciados de teoremas extraídos de arXiv y otras siete fuentes, que representa el corpus más grande disponible públicamente de teoremas de nivel de investigación creados por humanos. Representamos cada teorema con una breve descripción en lenguaje natural como representación para la recuperación y analizamos sistemáticamente cómo el contexto de la representación, la elección del modelo de lenguaje, el modelo de incrustación y la estrategia de *prompting* afectan la calidad de la recuperación. En un conjunto de evaluación curado de consultas de búsqueda de teoremas escritas por matemáticos profesionales, nuestro enfoque mejora sustancialmente tanto la recuperación a nivel de teorema como a nivel de artículo en comparación con los métodos de referencia existentes, lo que demuestra que la búsqueda semántica de teoremas es factible y efectiva a escala web. La herramienta de búsqueda de teoremas está disponible en https://huggingface.co/spaces/uw-math-ai/theorem-search{este enlace}, y el conjunto de datos está disponible en https://huggingface.co/datasets/uw-math-ai/TheoremSearch{este enlace}.
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}.