Research map / Large language models / Agents, code and math

Semantic Search over 9 Million Mathematical Theorems

NeurIPS 2026 · Large language models › Agents, code and math · approach: Retrieval-augmented formal theorem proving · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Builds a 9.2M-theorem corpus from arXiv and seven other sources, represents each theorem with an LLM-generated natural-language slogan, and embeds slogans with Qwen3-8B for semantic theorem search, beating ChatGPT 5.2 and Gemini 3 Pro on 111 mathematician-written queries.

Problem

Existing math search tools retrieve whole papers, while mathematicians and theorem-proving agents need specific theorems, lemmas, or propositions; semantic search behavior at this scale on research-level theorems is poorly understood.

Approach

Index each LaTeX theorem by an LLM-written natural-language slogan (with paper context) and retrieve via dense embeddings of informal queries, with binary-quantized HNSW search and reranking, rather than embedding raw LaTeX.

Key results

• Qwen3 8B with reranker reaches 45.0% theorem-level Hit@20 versus 27.0% for Gemini 3 Pro and 19.8% for ChatGPT 5.2 with search.
• Paper-level Hit@20 of 56.8% for the best system versus 37.8% for Google Search.
• Slogans generated with Body+First Section context raise Hit@20 from 73.7% (body only) to 76.3%; Claude Opus 4.5 slogans reach 84.2% Hit@20 vs 73.7% for DeepSeek V3.1 in the Body+Abstract setting.

Surprising findings

• Embedding raw LaTeX theorem statements performs far worse than embedding LLM-generated natural-language slogans (Gemma 0.3B: 9.0% vs 25.2% Hit@20).
• Abstract-only context for slogan generation did not improve over body-only context (73.7% both), while adding the first section helped.

Limitations

• Validation set is small (111 queries from 3 mathematicians, mostly algebraic geometry, analysis, PDEs), and the ablations use a 7,356-statement subset of math.AG papers.
• Baselines like Google and arXiv search are not designed for theorem-level retrieval, so comparisons are partly apples-to-oranges.
• Corpus is limited to arXiv papers with permissive licenses in the public release and contains parsing fragments from heuristic extraction.

Experimental setup

Datasets: arXiv theorems (9.2M) ProofWiki Stacks Project Open Logic Project CRing Project Stacks and Moduli HoTT Book An Infinitely Large Napkin

Benchmarks: 111-query validation set written by professional mathematicians

Metrics: Hit@1 Hit@10 Hit@20 MRR@20

Baselines: Google Search arXiv advanced search ChatGPT 5.2 with search Gemini 3 Pro Gemma 0.3B Qwen3 0.6B

Builds on: Qwen3-Embedding pgvector plasTeX Datasheets for Datasets

Closest papers by meaning

• RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematics (NeurIPS 2025 · similarity 0.87)
• Learning Theorem Rationale for Improving the Mathematical Reasoning Capability of Large Language Models (AAAI 2025 · similarity 0.87)
• ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Data (NeurIPS 2025 · similarity 0.86)
• OpenWebMath: An Open Dataset of High-Quality Mathematical Web Text (ICLR 2024 · similarity 0.86)
• Autoformalize Mathematical Statements by Symbolic Equivalence and Semantic Consistency (NeurIPS 2024 · similarity 0.84)
• Solving Inequality Proofs with Large Language Models (NeurIPS 2025 · similarity 0.84)