Math AI LabTheoremSearch/API Docs

API Reference

TheoremSearch exposes a REST API for semantic theorem search, dependency graph exploration, and paper lookup. All endpoints are available at the base URL below.

BASE URL

https://api.theoremsearch.com
GET

Graph

GET/graph?external_id={id}

Returns the full dependency graph for a paper, including its formal statements and directed edges.

QUERY PARAMETERS

FIELDTYPEDEFAULTDESCRIPTION
external_id*string—arXiv ID or other external paper identifier, e.g. 2403.05555.

EXAMPLE

curl "https://api.theoremsearch.com/graph?external_id=2403.05555"

RESPONSE

{
  "paper": {
    "paper_id": "uuid",
    "title": "Paper Title",
    "external_id": "2403.05555",
    "source": "arXiv",
    "url": "https://arxiv.org/abs/2403.05555",
    "authors": ["Author One", "Author Two"],
    "abstract": "..."
  },
  "statements": [
    {
      "statement_id": "uuid",
      "name": "Theorem 1.1",
      "body": "Let R be a ring...",
      "note": "Informal description or null",
      "proof": "Proof text or null"
    }
  ],
  "dependencies": [
    {
      "src_statement_id": "uuid",
      "src_name": "Theorem 1.1",
      "dep_statement_id": "uuid",
      "dep_name": "Lemma 2.3",
      "dep_paper_ext_id": "2401.00001",
      "dep_paper_title": "Another Paper",
      "interpaper": true
    }
  ]
}

interpaper: true on a dependency edge means the referenced statement lives in a different paper.

GET

Graph Embedding Search

GET/graph/embedding

Peform semantic search over the entire TheoremGraph corpus, formal and informal statements. Embeds the query with Qwen3-Embedding-8B and returns statements ranked by cosine similarity.

QUERY PARAMETERS

FIELDTYPEDEFAULTDESCRIPTION
query*string—Natural-language description of the mathematical result to find.
n_resultsinteger10Number of results to return.
formalitystring"both"Filter by corpus: "informal" (arXiv), "formal" (Lean), or "both".

EXAMPLE

curl "https://api.theoremsearch.com/graph/embedding?query=fundamental+theorem+of+calculus&n_results=5"

RESPONSE

{
  "results": [
    {
      "statement_id": "uuid",
      "name": "Theorem 1.1",
      "body": "If f is continuous on [a, b] and differentiable on (a, b)...",
      "slogan": "Every continuous function on a closed interval has an antiderivative.",
      "formality": "informal",
      "similarity": 0.943,
      "paper": {
        "title": "Real Analysis Notes",
        "external_id": "2301.00001",
        "source": "arXiv"
      }
    }
  ]
}
GET

Graph Statement

GET/graph/statement/{'{statement_id}'}

Returns a statement and its direct dependency neighborhood. Use the direction parameter to walk outward along dependency edges, and formality to select informal or formal edges.

PATH PARAMETER

FIELDTYPEDEFAULTDESCRIPTION
statement_id*string—UUID of the statement, obtained from /graph/embedding or /graph/paper.

QUERY PARAMETERS

FIELDTYPEDEFAULTDESCRIPTION
directionstring"both""src" (what this statement uses), "dep" (what uses this statement), or "both".
formalitystring"both""informal", "formal", or "both".

EXAMPLE

curl "https://api.theoremsearch.com/graph/statement/<statement_id>?direction=both&formality=formal"

RESPONSE

{
  "statement": {
    "statement_id": "uuid",
    "name": "Theorem 1.1",
    "body": "If f is continuous on [a, b]...",
    "slogan": "...",
    "formality": "formal"
  },
  "neighbors": [
    {
      "statement_id": "uuid",
      "name": "Lemma 2.3",
      "direction": "src",
      "edge_type": "proof",
      "formality": "formal"
    }
  ]
}
GET

Graph Paper

GET/graph/paper/{'{paper_id}'}

Returns all statements and dependency edges for an arXiv paper or Lean repository. Accepts either a UUID path parameter or an external_id query parameter for lookup by arXiv ID or repo slug.

PATH PARAMETER (OR QUERY PARAMETER)

FIELDTYPEDEFAULTDESCRIPTION
paper_idstring—UUID of the paper (path parameter).
external_idstring—arXiv ID or Lean repo slug, e.g. 2301.00001 or leanprover-community/mathlib4.

EXAMPLE

curl "https://api.theoremsearch.com/graph/paper?external_id=2301.00001"

RESPONSE

{
  "paper": {
    "paper_id": "uuid",
    "title": "Real Analysis Notes",
    "external_id": "2301.00001",
    "source": "arXiv"
  },
  "statements": [
    {
      "statement_id": "uuid",
      "name": "Theorem 1.1",
      "body": "If f is continuous on [a, b]...",
      "slogan": "...",
      "formality": "informal"
    }
  ],
  "dependencies": [
    {
      "src_statement_id": "uuid",
      "dep_statement_id": "uuid",
      "edge_type": "proof",
      "formality": "informal"
    }
  ]
}

Tip: search with /graph/embedding to get a statement_id, then walk its neighborhood with /graph/statement/{id}.

MCP

TheoremSearch is available as an MCP (Model Context Protocol) server for AI agents. It exposes a single tool theorem_search with the same parameters as POST /search.

ENDPOINThttps://api.theoremsearch.com/mcp

EXAMPLE — CALL theorem_search VIA MCP

curl -X POST https://api.theoremsearch.com/mcp \
  -H "Content-Type: application/json" \
  -d '{
    "jsonrpc": "2.0",
    "id": "1",
    "method": "tools/call",
    "params": {
      "name": "theorem_search",
      "arguments": {
        "query": "every projective module over a local ring is free",
        "n_results": 5
      }
    }
  }'

RESPONSE

{
  "jsonrpc": "2.0",
  "id": "1",
  "result": {
    "content": [{ "type": "text", "text": "{...serialized SearchResponse...}" }],
    "structuredContent": { "theorems": [...] }
  }
}

SUPPORTED METHODS

FIELDTYPEDEFAULTDESCRIPTION
initialize——Handshake. Returns protocol version and server capabilities.
tools/list——Returns the theorem_search tool schema.
tools/call——Invokes theorem_search with the given arguments.