TheoremSearch-MCP

An MCP wrapper for TheoremSearch (UW Math AI Lab), which semantically searches about 9.27 million mathematical statements across 8 sources including arXiv, Stacks Project, and ProofWiki.

This repository provides two integration paths:

Quick Test (No MCP Setup Needed)

If you just want to evaluate search quality first, run the script (only requests is required).

Use the Python executable inside the virtual environment directly (recommended), so you do not need activation-specific shell commands.

Windows (PowerShell/CMD):

python -m venv .venv
.venv\Scripts\python -m pip install -r requirements.txt
.venv\Scripts\python scripts\quick_test.py

macOS/Linux (bash/zsh):

python3 -m venv .venv
.venv/bin/python -m pip install -r requirements.txt
.venv/bin/python scripts/quick_test.py

It demonstrates semantic search, filtered search (source/type/year), whole-corpus graph search (including formal Lean), paper autocomplete, and dependency graph traversal.

You can also call the API directly with curl:

curl -s -X POST https://api.theoremsearch.com/search -H "Content-Type: application/json" -d '{"query":"Any projective module over a local ring is free","n_results":3}'

Related MCP server: mathlas

Path A: Official Remote MCP (Fastest)

Codex

Add this to .codex/config.toml in your target project:

[mcp_servers.theoremsearch_remote]
url = "https://api.theoremsearch.com/mcp"
tool_timeout_sec = 120

VS Code (GitHub Copilot / MCP-capable clients)

Create .vscode/mcp.json in the project:

{
  "servers": {
    "theoremsearch-remote": {
      "type": "http",
      "url": "https://api.theoremsearch.com/mcp"
    }
  }
}

Claude Desktop

Add this to claude_desktop_config.json:

{
  "mcpServers": {
    "theoremsearch-remote": {
      "type": "http",
      "url": "https://api.theoremsearch.com/mcp"
    }
  }
}

The official remote MCP exposes a single tool, theorem_search, with parameters matching POST /search (including sources, types, year_range, citation_range, citation_weight, etc.), and supports initialize / tools/list / tools/call.

Path B: Local MCP Wrapper (This Repo, Recommended)

This wrapper provides 5 tools, adding graph capabilities beyond the official MCP:

Install and Run

Windows (PowerShell/CMD):

python -m venv .venv
.venv\Scripts\python -m pip install -r requirements.txt

macOS/Linux (bash/zsh):

python3 -m venv .venv
.venv/bin/python -m pip install -r requirements.txt

Virtual environment path differences:

• Windows executables are under .venv\\Scripts\\.

• macOS/Linux executables are under .venv/bin/.

After activating your virtual environment, add this to .codex/config.toml in the target project:

[mcp_servers.theoremsearch]
command = "python"
args = ["-E", "./server.py"]
cwd = "./"
tool_timeout_sec = 120

-E ignores PYTHONPATH, preventing a local mcp/ directory from shadowing the official MCP SDK required by fastmcp.

For VS Code, use .vscode/mcp.json:

{
  "servers": {
    "theoremsearch-local": {
      "type": "stdio",
      "command": "python",
      "args": ["-E", "${workspaceFolder}/server.py"]
    }
  }
}

You can also manually run the server in stdio mode for validation:

.venv\Scripts\python -E .\server.py

.venv/bin/python -E ./server.py

Usage Examples

Use theorem-like statements as queries (more complete statements usually work better):

theorem_search(query="Any projective module over a local ring is free", n_results=5)

Filtered search example (lemmas in Stacks Project after 2010):

theorem_search(query="smooth DM stack has a dense open subscheme", sources=["Stacks Project"], types=["Lemma"], year_range=[2010, 2024])

Citation-weighted search example (highly cited classical results):

theorem_search(query="Hahn-Banach separation theorem", citation_weight=0.5, citation_range=[100, 5000])

Two-step dependency-graph workflow: first get a statement_id from whole-corpus graph search, then traverse dependencies (graph_statement accepts informal or formal, not both):

graph_search(query="any projective module over a local ring is free", formality="both", n_results=1)
graph_statement(statement_id="<statement_id from previous step>", direction="both", formality="informal")

Notes

• Public API examples do not require an API key, but production rate limits are not publicly specified. Control request frequency (for example, global serialized 1 req/s).

• Default request timeout is 180s (/graph/embedding with formality=formal can exceed 60s in practice). Large n_results or db_top_k increases latency.

• year_range and citation_range should be 2-item arrays: [min, max].

• There are a few live-API vs doc mismatches (corrected here based on observed behavior): /graph/statement accepts only informal/formal; response shape is {root, nodes, edges} instead of documented {statement, neighbors}; /graph/paper returns {paper, statements, edges} instead of {..., dependencies}. Recheck if upstream APIs change.