Semantic Search over 9 Million Mathematical Theorems

Luke Alexander, Eric Leonen, Sophie Szeto, Artemii Remizov, Ignacio Tejeda, Giovanni Inchiostro, Vasily Ilin

---

Overview Mathematicians and math prover agents need fast and efficient theorem search. We release Theorem Search over all of arXiv, the Stacks Project, and six other sources. Our search is 2× more accurate than frontier LLMs, with only 4 second latency. Feedback is welcome. Retrieval Performance (Hit@10) Model Theorem-level Paper-level Google Search — 0.378 ChatGPT 5.2 0.180 — Gemini 3 Pro 0.252 — Ours 0.432 0.505 Theorem-level = retrieval of exact theorem statements Paper-level = retrieval of the correct paper containing the theorem

---

API

TheoremSearch provides a production REST API for semantic theorem search.Example:

curl https://api.theoremsearch.com/search \
  -H "Content-Type: application/json" \
  -d '{
        "query": "smooth DM stack codimension one",
        "n_results": 5
      }'

Returns a JSON object containing theorem-level results with metadata and similarity scores.

MCP

TheoremSearch is also available as an MCP tool for AI agents with a single tool theorem_search. Endpoint: https://api.theoremsearch.com/mcp.

---

Citation

@article{alexander2026semantic,
  title  = {Semantic Search over 9 Million Mathematical Theorems},
  author = {Alexander, Luke and Leonen, Eric and Szeto, Sophie and Remizov, Artemii and Tejeda, Ignacio and Inchiostro, Giovanni and Ilin, Vasily},
  journal= {arXiv preprint arXiv:2602.05216},
  year   = {2026},
  doi    = {10.48550/arXiv.2602.05216},
  url    = {https://arxiv.org/abs/2602.05216}
}