Semantic Search over 9 Million Mathematical Theorems

This paper introduces a scalable semantic search system for a corpus of 9.2 million mathematical theorems, demonstrating that representing theorems with natural-language descriptions significantly improves retrieval accuracy for both specific theorems and entire papers compared to existing baselines.

The Gist

Imagine the world of mathematics as a massive, chaotic library containing 9.2 million books. But here's the catch: these aren't normal books with chapters and stories. They are filled with dense, technical formulas, symbols, and theorems (the "rules" of math).

Currently, if you walk into this library and ask a librarian (or a search engine like Google) for a specific rule—say, "How do I calculate the area of a weird shape?"—they will hand you entire books that might contain the answer. You then have to spend hours flipping through pages, scanning for the one sentence you actually need. It's like trying to find a specific needle in a haystack by reading the entire haystack.

This paper introduces a new way to search this library. Here is the simple breakdown of what they did:

1. The Problem: The "Needle in a Haystack"

Mathematicians and AI agents often need to find a single specific rule (a theorem) to solve a problem. But existing tools are stuck at the "book level." They can tell you which paper to read, but they can't point you to the exact sentence inside that paper. This leads to wasted time and, worse, AI systems inventing fake rules because they couldn't find the real one.

2. The Solution: The "Slogan" Strategy

The authors built a massive database of 9.2 million mathematical rules. But instead of searching the raw, scary math symbols (like $\int x^2 dx$), they used AI to translate every single rule into a short, plain-English "slogan."

• Old Way: Searching for the raw code of a theorem.
• New Way: Searching for a human-friendly summary.

The Analogy: Imagine every theorem in the library has a movie poster hanging outside it.

• The movie is the complex math paper (hard to read).
• The poster is the "slogan" (e.g., "This rule proves that all triangles on a sphere have angles adding up to more than 180 degrees").

When you ask a question, the system doesn't read the whole movie; it matches your question to the movie posters.

3. How They Built It

• The Collection: They scraped 9.2 million rules from the internet (mostly from arXiv, a giant repository of scientific papers).
• The Translator: They used a super-smart AI (a Large Language Model) to read every single math rule and write a 1-4 sentence summary in plain English.
• The Index: They turned these summaries into a giant digital map where similar ideas are close together.

4. The Results: Finding the Needle Instantly

They tested this system against the best tools currently available (Google, ChatGPT, and specialized math search engines).

• The Test: Professional mathematicians asked 111 specific questions about rules they knew existed but couldn't easily find.
• The Outcome: Their new system found the correct rule 45% of the time in the top 20 results.
• The Competition: Google Search and ChatGPT only found the right rule about 20% of the time.

Why it worked better:
Google looks at the title and abstract of a paper. But many important rules are buried deep inside a paper, far from the title. Because this new system reads and summarizes every single rule in the paper, it can find a tiny, obscure rule buried on page 40 just as easily as a famous rule on page 1.

5. Why This Matters

• For Humans: It saves researchers hours of digging. You can ask, "Is there a rule about X?" and get the exact rule, not a list of 50 papers to read.
• For AI: AI agents trying to prove math theorems often get stuck because they can't find the right "tools" (lemmas) to use. This system acts like a perfect toolbox, handing the AI the exact tool it needs to keep building.
• The "RAG" Effect: In one experiment, an AI was asked a hard math question. Without this tool, it confidently gave a wrong answer. When given access to this "slogan library," it found the right rule and gave the correct answer.

The Bottom Line

The authors have built a Google for specific math rules. Instead of searching for "books about math," you can now search for "the specific rule that says X." They turned a library of 9 million complex documents into a searchable list of simple, human-readable summaries, making the world's mathematical knowledge much easier to find and use.

You can try it yourself at theoremsearch.com.

Technical Summary

Here is a detailed technical summary of the paper "Semantic Search over 9 Million Mathematical Theorems".

1. Problem Statement

Mathematical knowledge is fundamentally organized around discrete results (theorems, lemmas, propositions), yet existing search tools (Google Scholar, arXiv, and general-purpose LLMs) operate at the document level.

• The Gap: Researchers and AI agents often need to find a specific theorem statement, not just the paper containing it. Current tools force users to manually scan entire PDFs to locate specific results.
• Consequences: This leads to inefficiency and errors. The paper cites instances where authors retracted papers because their results were already established, and AI systems "solving" problems that had been solved decades earlier, simply because they failed to retrieve the specific prior theorem.
• Technical Challenge: Mathematical text is highly symbolic (LaTeX). Standard semantic search models struggle with dense notation, and direct embedding of raw LaTeX often fails to capture the semantic intent of a query written in natural language.

2. Methodology

The authors constructed a unified corpus and a retrieval pipeline designed to bridge the gap between informal natural language queries and formal mathematical statements.

A. Data Collection & Corpus Construction

• Scale: The dataset contains 9.2 million theorem statements, representing the largest publicly available collection of human-authored, research-level theorems.
• Sources:
  • 99.5% from arXiv (tagged math, stat, cs, physics, etc.).
  • 0.5% from curated sources: Stacks Project, ProofWiki, Open Logic Project, CRing Project, HoTT Book, and An Infinitely Large Napkin.
• Parsing Pipeline: To extract theorems from raw LaTeX, three strategies were employed:
  1. Node Search (plasTeX): Converts LaTeX to a node tree to identify theorem environments (successful for ~6.9M theorems).
  2. TeX Logging: A custom package injected during compilation to log theorem data (fallback for ~1.8M theorems).
  3. Regex Parsing: Identifies delimiters like \begin{theorem} (fallback for ~0.5M theorems).
• Representation (The "Slogan"): Instead of embedding raw LaTeX, the system uses an LLM (DeepSeek V3) to generate a short, natural-language description (a "slogan") for each theorem.
  • Constraints: Slogans are declarative, avoid symbols/proofs, and are limited to 4 sentences.
  • Context Variations: The authors tested three prompting strategies: Body Only, Body + Abstract, and Body + Introduction.

B. Retrieval Architecture

• Embedding: Theorem slogans and user queries are embedded into a shared vector space using Qwen3-Embedding-8B.
• Indexing: Vectors are stored in a PostgreSQL database with the pgvector extension, utilizing a Hierarchical Navigable Small World (HNSW) index combined with binary quantization for fast approximate nearest-neighbor search.
• Two-Stage Retrieval:
  1. Candidate Generation: Fast retrieval of top-$k$ candidates based on Hamming distance (after binary quantization).
  2. Re-ranking: Candidates are re-ranked using Cosine Similarity on the original high-dimensional vectors. A cross-encoder reranker (Qwen3-Reranker-0.6B) was also tested to improve fine-grained semantic matching.

C. Evaluation

• Validation Set: A curated set of 111 queries written by professional mathematicians. Crucially, these queries were written "blind" (from memory) to prevent data leakage.
• Baselines: Compared against Google Search, arXiv advanced search, ChatGPT 5.2 (with search), and Gemini 3 Pro.
• Metrics: Hit@k (Hit Rate) and Mean Reciprocal Rank (MRR) at both the theorem level (exact statement match) and paper level (paper containing the statement).

3. Key Contributions

1. Largest Theorem Corpus: Release of a 9.2M theorem dataset with rich metadata, including source URLs and LaTeX bodies.
2. Slogan-Based Representation: Demonstrated that converting formal theorems into natural language "slogans" significantly outperforms embedding raw LaTeX.
3. Systematic Ablation Studies:
   • Context Matters: Providing the LLM with the paper's Introduction (not just the abstract or body) yields the best slogan quality and retrieval performance.
   • Model Choice: Proprietary models (Claude Opus 4.5, Gemini 3 Pro) generated better slogans than open-source models, but Qwen3 8B as an embedder provided the best retrieval performance.
   • Prompting: Explicit task instructions for the embedder improved performance for Qwen models.
4. State-of-the-Art Performance: The system achieves superior retrieval metrics compared to current industry standards.

4. Results

On the 111-query validation set:

• Theorem-Level Retrieval (Hit@20):
  • Qwen3 8B (Best Method): 45.0%
  • Gemini 3 Pro: 27.0%
  • ChatGPT 5.2 w/ Search: 19.8%
  • Google Search: N/A (cannot return specific theorems)
• Paper-Level Retrieval (Hit@20):
  • Qwen3 8B: 56.8%
  • Google Search: 37.8%
• Qualitative Findings:
  • The system successfully retrieves auxiliary lemmas deep within papers that are missed by abstract-based search.
  • RAG Experiment: When used as a Retrieval-Augmented Generation (RAG) tool for Claude, the system corrected a confident but incorrect mathematical argument regarding KSBA compactifications, proving its utility in preventing LLM hallucinations.
  • Latency: The search tool returns results in 3 seconds, significantly faster than LLM-based tools that perform multiple web searches (60+ seconds).

5. Significance and Impact

• Feasibility of Semantic Theorem Search: The paper proves that semantic search over millions of research-level mathematical theorems is feasible and effective at web scale.
• Tooling for AI and Humans:
  • For Mathematicians: Enables rapid literature review and verification of specific results without scanning full papers.
  • For AI Agents: Provides a critical tool for premise selection in automated theorem proving and prevents AI from "re-discovering" known results or hallucinating proofs.
• Open Access: The authors have released the dataset, a public search interface (HuggingFace), a REST API, and an MCP (Model Context Protocol) server, allowing integration into AI workflows.

Conclusion

This work addresses a critical bottleneck in mathematical research and AI reasoning: the inability to search for specific logical statements within a sea of documents. By leveraging LLMs to translate formal notation into natural language "slogans" and utilizing advanced dense retrieval, the authors have created a system that outperforms existing tools by a wide margin, offering a new paradigm for accessing mathematical knowledge.