Busca Semântica em Mais de 9 Milhões 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
Resumo
A busca por resultados matemáticos continua difícil: a maioria das ferramentas existentes recupera artigos inteiros, enquanto matemáticos e agentes de prova de teoremas frequentemente buscam um teorema, lema ou proposição específica que responda a uma consulta. Embora a busca semântica tenha registrado progressos rápidos, o seu comportamento em corpora grandes e altamente técnicas, como teoremas matemáticos de nível de pesquisa, permanece pouco compreendido. Neste trabalho, introduzimos e estudamos a recuperação semântica de teoremas em larga escala sobre um corpus unificado de 9,2 milhões de enunciados de teoremas extraídos do arXiv e de sete outras fontes, representando o maior corpus publicamente disponível de teoremas de nível de pesquisa de autoria humana. Representamos cada teorema com uma breve descrição em linguagem natural como uma representação para recuperação e analisamos sistematicamente como o contexto da representação, a escolha do modelo de linguagem, o modelo de incorporação e a estratégia de *prompting* afetam a qualidade da recuperação. Num conjunto de avaliação curado de consultas de busca por teoremas escritas por matemáticos profissionais, a nossa abordagem melhora substancialmente a recuperação tanto a nível de teorema como a nível de artigo em comparação com as *baselines* existentes, demonstrando que a busca semântica de teoremas é viável e eficaz em escala web. A ferramenta de busca de teoremas está disponível em https://huggingface.co/spaces/uw-math-ai/theorem-search{este *link*}, e o conjunto de dados está disponível em https://huggingface.co/datasets/uw-math-ai/TheoremSearch{este *link*}.
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}.