Source-linked AI summary
Semantic Search over 9 Million Mathematical Theorems
Luke Alexander, Eric Leonen, Sophie Szeto, Artemii Remizov, Ignacio Tejeda, Jarod Alper, Giovanni Inchiostro, Vasily Ilin
TL;DR
Existing search tools usually retrieve whole papers, leaving theorem-level retrieval on large mathematical corpora poorly understood. The paper constructs a 9.2-million-theorem corpus and studies natural-language representations and embedding choices for semantic retrieval. On mathematician-written queries, the best configuration achieves 45.0% theorem-level Hit@20 and 56.8% paper-level Hit@20, outperforming the reported baselines.
Problem
Existing tools retrieve entire papers rather than specific theorems, while semantic retrieval for large, technical mathematical corpora remains poorly understood.
Method
The authors build a corpus of over 9 million theorem statements, generate LLM-based natural-language slogans, embed slogans and queries, and systematically vary representation context and retrieval models.
Results
45.0% theorem-level Hit@20 and 56.8% paper-level Hit@20 were achieved on 111 mathematician-written queries, outperforming the reported baselines.
Takeaways & Limitations
Treating theorems as first-class retrieval objects enables access to mathematical knowledge for expert search, retrieval-augmented generation, and formal proof premise selection.
Takeaways & Limitations
Evaluation baselines are not designed for theorem-level retrieval, and incorrect reference numbers count as theorem misses but paper matches.
Abstract
from arXiv · showhide
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.
1. Introduction
Mathematical knowledge is organized around theorem-level results, but existing search tools retrieve entire papers rather than specific statements. This work addresses that gap with a 9-million-theorem corpus and natural-language slogan representations for semantic retrieval.
- Theorems, lemmas, propositions, and corollaries are fundamental reasoning units for mathematicians and automated proof systems.
- Existing tools operate at the document level, forcing users to manually scan papers for specific mathematical statements.
- 2.5% of more than 14,000 withdrawn arXiv preprints were retracted because their results already appeared in prior literature.
- The authors construct a corpus of over 9 million theorem statements from arXiv, the Stacks Project, ProofWiki, and five other sources.
- Natural-language slogans generated by an LLM represent theorems in a shared semantic space with user queries.
- The study systematically evaluates how context, LLM choice, embedding model, and prompting strategy affect retrieval quality.
3. State-of-the-art retrieval. On 111 queries from pro-
On 111 professional-mathematician queries, the system outperformed general-purpose search and language-model baselines for theorem- and paper-level retrieval. These results support semantic theorem search at web scale.
- 45.0% Hit@20 at the theorem level outperformed ChatGPT 5.2 with search at 19.8% and Gemini 3 Pro at 27.0%.
- 56.8% Hit@20 at the paper level exceeded Google Search at 37.8%.
- The results demonstrate that semantic theorem search is feasible at web scale.
2. Related Work
Prior work advanced formula retrieval, dense retrieval, formal-mathematics search, and paper-level literature search, but semantic retrieval of mathematical statements remains an open challenge. This work extends natural-language theorem retrieval to millions of informal LATEX statements.
- MathIR benchmarks established formula-level retrieval and mathematical question answering, while semantic understanding of mathematical statements remains an open challenge.
- Dense retrieval and late-interaction methods provide foundations for efficient semantic similarity and fine-grained matching.
- Formal-mathematics systems use natural-language descriptions, dense retrieval, premise selection, and intent modeling to search theorem libraries.
- This work extends informalization-based retrieval to millions of LATEX theorem statements.
- General academic search engines and web-enabled language models retrieve papers but cannot reliably target individual theorems.
3. Data Collection
The dataset combines parsed theorem statements from arXiv and several open mathematical sources, then enriches them with natural-language slogans and vector embeddings for search. The authors evaluate retrieval on 111 queries written by research mathematicians.
- Pipeline: Figure 1 summarizes the pipeline from theorem parsing through natural-language representation and embedding for retrieval.
- Corpus: 99.5% of the 9.2 million theorems come from arXiv papers tagged in mathematics, statistics, computer science, physics, engineering, economics, quantitative finance, or quantitative biology.
- Representation: Theorem names contain a type, an optional reference number, and an optional note, while bodies contain LATEX content with basic author-defined macros expanded.
- Theorem Parsing: The arXiv pipeline uses plasTeX node search, TeX logging, and regex parsing to handle varied theorem environments.
- Other Sources: The remaining 0.5% of the corpus comes from ProofWiki, the Stacks Project, Open Logic Project, CRing Project, Stacks and Moduli, the HoTT Book, and An Infinitely Large Napkin.
- Slogan Generation: LLM-generated slogans convert formal theorem statements into searchable natural-language representations, with body-only, body-plus-abstract, and body-plus-introduction variants.
- Embedding and Retrieval: Slogans and queries are embedded with Qwen3-Embedding-8B, retrieved using HNSW and Hamming distance, then reranked by cosine similarity.
- Evaluation: Three research mathematicians wrote 111 blind queries across 14 arXiv tags to evaluate retrieval of known mathematical results.
4. Experiments
The experiments evaluate theorem-level and paper-level retrieval against existing tools, then test reranking, ranking diversity, retrieval-augmented reasoning, and representation choices. Qwen3 8B performs strongly, while richer context and model-specific slogan generation and embedding instructions affect retrieval quality.
- Main results: Qwen3 8B outperforms existing literature-review methods across retrieval metrics, with higher Hit@10 and Hit@20 indicating effective candidate discovery.A cross-encoder reranker further improves theorem-level Hit@1 from 17.1% to 18.9% and MRR@20 from 24.3% to 27.0%.
- Main results: Qwen3 8B also outperforms baseline models at paper-level retrieval, while arXiv search finds only two papers in the top 20 across the query set.Google and arXiv cannot return individual theorem statements, so they are evaluated only at the paper level.
- Main results: ChatGPT and Gemini often rank multiple theorems from one paper consecutively, reducing result diversity and lowering Hit@k despite sometimes achieving high early precision.Gemini returns an average of 10.98 distinct papers per query.
- Main results: Independent theorem indexing makes the system particularly useful for auxiliary lemmas and technical results buried deep within papers, beyond title- and abstract-based metadata.The approach indexes each theorem through its natural-language slogan, rather than relying primarily on paper-level metadata.
- Retrieval-augmented reasoning: Retrieval augmentation corrected Claude’s initially incorrect answer about KSBA compactifications by retrieving relevant theorems and supporting a valid cited reasoning chain.Without retrieval, Claude claimed all boundary pairs retain a fibration; with retrieval, it identified pseudoelliptic surfaces formed by contracting the section.
- Ablation studies: Adding the first paper section to slogan-generation context improves retrieval over abstract-only context, because additional context better captures theorem intent.The ablation uses a restricted corpus of 7,356 statements from eight primary authors.
- Ablation studies: Slogan-generation quality varies by LLM, with Claude Opus 4.5 and Gemini 3 Pro outperforming DeepSeek-V3 in the reported comparison.The paper attributes this difference to variation in mathematical-text training and the quality of informal theorem descriptions.
- Ablation studies: Math retrieval instructions improve both Qwen embedders, whereas Gemma performs better with empty instructions, though still worse than instructed Qwen3 8B.The result shows that prompting effects depend on the embedding model.
5. Search Tool
The search tool supports natural-language theorem retrieval through a two-stage architecture, metadata filtering, reranking, and multiple access interfaces. Query duplication addresses the mismatch between short keyword queries and slogan embeddings.
- Access: The project exposes theorem search through a web interface, REST API, and MCP server for research workflows and AI-agent reasoning.The API accepts JSON queries and returns ranked theorem results.
- Retrieval architecture: The tool encodes natural-language queries with Qwen3-8B embeddings, retrieves candidates using HNSW and Hamming distance, then filters and reranks them.The initial pool is bounded between 200 and 800 candidates before cosine-similarity reranking.
- User interface: The interface displays theorem slogans, rendered theorem bodies, paper metadata, and paper links, while allowing metadata filtering and relevance feedback.Filters include author sets, arXiv categories, and journal publication status.
- Retrieval architecture: Citation-weighted retrieval reranks candidates with cosine similarity plus a logarithmic citation term controlled by λ.The citation-weight parameter is user-specified.
- Query handling: Repeating short keyword queries strengthens key-term signals when multi-sentence slogan embeddings otherwise dilute them with padding or generic context.The tool applies this duplication automatically.
6. Conclusion
The paper addresses document-level search that forces users to locate individual mathematical statements manually by building a 9.2-million-theorem corpus and evaluating slogan-based semantic retrieval. Its best configuration improves theorem- and paper-level retrieval and supports access for mathematicians and automated proof systems.
- Problem: Existing search tools operate at the document level, forcing researchers and AI agents to manually locate specific theorems, lemmas, propositions, and corollaries.The paper frames these discrete results as the basic units of mathematical knowledge.
- Contribution: The authors construct a unified corpus of over 9.2 million human-authored, research-level theorem statements from arXiv and seven other sources.They describe it as the largest unified collection of its kind to date.
- Results: 45.0% theorem-level Hit@20 and 56.8% paper-level Hit@20 are achieved on 111 mathematician-written queries, outperforming the named search baselines.The baselines include ChatGPT 5.2 with search, Gemini 3 Pro, and Google Search.
- Representation: Natural-language LLM-generated slogans outperform raw LATEX representations, while slogan context, generating LLM, and embedding model affect retrieval quality.Slogans generated with access to paper introductions outperform those generated from theorem bodies alone.
- Implications: The system provides theorem-level access for LLM retrieval-augmented generation, formal proof premise selection, and expert literature review.The paper also reports qualitative feedback from research mathematicians about practical utility.
A. Datasheet
The dataset unifies millions of mathematical theorems with source metadata for semantic search, while documenting collection, preprocessing, licensing, maintenance, and known data limitations.
- Dataset composition: 9.2 million mathematical statements are included in the dataset.
- Dataset composition: The dataset is a non-random collection from available mathematical corpora, including most arXiv theorems and all theorems from several other sources.
- Dataset composition: Each instance records a theorem’s source name, raw TeX body, author-written label, source paper, and document metadata.
- Limitations: Some theorem bodies, titles, and labels may be fragmented because parsing methods do not support every TeX document.
- Collection and preprocessing: Theorems were parsed with plasTeX, custom TeX logging, and regex fallbacks, then cleaned by expanding simple macros and filtering corrupted bodies.
- Uses and distribution: The dataset supports a semantic search engine for mathematicians and automated theorem-proving agents and is publicly distributed under inherited source licenses.
B.2. Feedback Two
A user sought a precise citation for a known result whose existing references were indirect; theorem search located a directly connected result with fewer queries.
- The tool found a result whose citation list directly referenced the user’s target theorem.
- The user located the desired theorem with fewer queries than traditional search methods, which had returned only indirect references.
- The use case involved a result known to experts but lacking a specific citable reference.
C. Claude Experiment
The Claude experiment contrasts an incorrect answer without retrieval against a correct, theorem-grounded answer with the theorem database, while exposing disagreement about KSBA boundary fibrations.
- Without RAG: Without retrieval augmentation, Claude incorrectly concluded that every KSBA boundary pair retains a fibration with one-dimensional fibers.
- Fibration argument: A competing argument states that the boundary divisor preserves a fibration over a nodal curve with one-dimensional fibers.
- With RAG: With retrieval augmentation, Claude correctly identified boundary pairs as pseudoelliptic surfaces obtained by contracting the section.
- With RAG: The retrieved response cited specific theorem numbers and supplied a logically valid chain of reasoning grounded in retrieved results.
- With RAG: The cited results include an explicit KSBA-stable pseudoelliptic family on the boundary, showing that the queried type of boundary pair exists.
D. Validation Set arXiv Categories
The validation set spans 12 of arXiv’s 32 mathematics tags, while the accompanying tables describe category distributions in the validation set and the full dataset.
- The validation set covers 12 of arXiv’s 32 mathematics tags across 65 unique papers.
- Table 6 reports arXiv-category counts for the validation set using primary-category and all-cross-listed-paper views.
- Table 7 reports the corresponding arXiv-category distributions for the whole dataset.
E. More Experiments
The section expands the experiments to additional embedding models and reports extended retrieval results for context-window size and LLM-generated slogans. It also documents the prompts and task instructions used for slogan generation and retrieval baselines.
- Additional embedders: The experiments include Multilingual-E5-Large-Instruct, zbMath-Bert, and KaLM-Embedding-V2.5 among a larger set of embedders.These models are explicitly listed as additions to the experimental embedder set.
- Extended retrieval experiments: Extended results compare retrieval performance across context-window sizes without task instructions.This comparison is identified in the caption for Table 8.
- Extended retrieval experiments: Extended results compare LLM-generated slogans for retrieval using body and abstract text without task instructions.This comparison is identified in the caption for Table 9.
- Prompting setup: The retrieval prompt requests the top 20 most relevant mathematical statements for each query.The prompt also requires arXiv provenance, statement numbering, section information, descriptors, and relevance notes.
- Prompting setup: Prompt instructions require arXiv statements and the most recent available arXiv version, while allowing unverifiable numbering to be marked UNVERIFIED.Separate instructions specify immediate answering and web or Google Search grounding to verify statement numbering.