Semantic Search over 9 Million Mathematical Theorems

Luke Alexander, Eric Leonen, Sophie Szeto, Artemii Remizov, Ignacio Tejeda, Jarod Alper, 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

@inproceedings{alexander2026semantic,
  author        = {Alexander, Luke and Leonen, Eric and Szeto, Sophie and Remizov, Artemii and Tejeda, Ignacio and Alper, Jarod and Inchiostro, Giovanni and Ilin, Vasily},
  title         = {Semantic Search over 9 Million Mathematical Theorems},
  booktitle     = {Advances in Neural Information Processing Systems},
  volume        = {39},
  year          = {2026},
  note          = {Evaluations and Datasets Track},
  archivePrefix = {arXiv},
  eprint        = {2602.05216},
  primaryClass  = {cs.IR},
  url           = {https://arxiv.org/abs/2602.05216}
}

@article{kurgan2026theoremgraph,
  title         = {TheoremGraph: Bridging Formal and Informal Mathematics},
  author        = {Kurgan, Simon and Wang, Evan and Leonen, Eric and Szeto, Sophie and Alexander, Luke and Remizov, Artemii and Alper, Jarod and Inchiostro, Giovanni and Ilin, Vasily},
  journal       = {arXiv preprint arXiv:2606.25363},
  year          = {2026},
  eprint        = {2606.25363},
  archivePrefix = {arXiv},
  primaryClass  = {cs.IR},
  url           = {https://arxiv.org/abs/2606.25363}
}