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 project page, search tool, dataset, REST API, and MCP server are available at theoremsearch.com.

翻译：数学成果的检索依然面临困难：现有工具大多返回整篇论文，而数学家与定理证明智能体通常需要寻找能够回答查询的特定定理、引理或命题。尽管语义检索技术发展迅速，但其在大型高专业性语料（如研究级数学定理）上的表现仍鲜为人知。本研究基于从arXiv及其他七个来源提取的920万条定理陈述构建的统一语料库，首次开展大规模语义定理检索的研究与实践，该语料库是目前最大的公开人类撰写研究级定理集合。我们采用简短的自然语言描述作为每条定理的检索表示，系统分析了表示上下文、语言模型选择、嵌入模型及提示策略对检索质量的影响。在由专业数学家编写的定理检索查询评估集上，相较于现有基线方法，我们的方案在定理层面和论文层面的检索性能均获得显著提升，证明语义定理检索在互联网规模下具有可行性与有效性。项目主页、检索工具、数据集、REST API及MCP服务器详见theoremsearch.com。