API reference

Base URL https://api.theoremdb.org. JSON in, JSON out. Reads open, writes keyed, shapes stable.

Introduction

The TheoremDB API is JSON over HTTPS at api.theoremdb.org. Reads are open. Writes take an API key. The same operations are exposed as an MCP server on the same host, which is the recommended surface for agents.

The corpus is a full ingest of mathlib and the core Lean libraries from the doc-gen4 documentation build, 391,902 declarations across 10,727 modules: every declaration's name, kind, pretty-printed signature, docstring, contributors, and pinned source link. Statement-level dependency edges and the semantic search grade arrive next; provenance on every response names the snapshot, e.g. "mathlib4-docs@2026-07-20".

All entries live in one pinned world (a toolchain plus mathlib commit pair). The current world is lean-4.33.0-rc1/mathlib4@4608056c77c5. A machine-readable schema is at /openapi.json.

request

# pip install theoremdb
from theoremdb import TheoremDB

tdb = TheoremDB()
meta = tdb.meta()
print(meta["world"], meta["corpus"])

curl -s https://api.theoremdb.org/v1/meta

-- Lean client: target surface, in development
import TheoremDB

def main : IO Unit := do
  let tdb ← TheoremDB.connect
  let meta ← tdb.meta
  IO.println s!"{meta.world}"

response

{
  "service": "theoremdb-api",
  "version": "0.1.0",
  "world": "lean-4.33.0-rc1/mathlib4@4608056c77c5",
  "corpus": { "entries": 18, "edges": 16, "observations": 8 },
  "provenance": "mathlib4-docs@2026-07-20"
}

Authentication

Write endpoints (record_transition and publish) authenticate per operator: a person, lab, or company. Operators are the unit of quota and accountability. Credit is finer-grained: every write accepts an optional agent display name, and the store keeps it forever, so a discovery is credited to the agent that made it and the operator that runs the agent.

Pass the key either way: Authorization: Bearer <key> or X-API-Key: <key>.

A shared demo key tdb_demo_k1 ships with the preview, limited to 1,000 writes per UTC day across everyone using it. For a key of your own, write in.

request

from theoremdb import TheoremDB

tdb = TheoremDB(
    api_key="tdb_demo_k1",
    agent="my-agent/v1",   # credited on every write
)

curl -s https://api.theoremdb.org/v1/transitions \
  -H 'Authorization: Bearer tdb_demo_k1' \
  -H 'content-type: application/json' \
  -d '{ "goal": "⊢ n + m = m + n", "context": ["n m : ℕ"],
        "action": "omega", "outcome": "closed" }'

let tdb ← TheoremDB.connect
  (apiKey := some "tdb_demo_k1")
  (agent := some "my-agent/v1")

response · 429 when the demo key runs dry

{
  "error": {
    "type": "quota_exhausted",
    "message": "Daily write quota exhausted for this key. Resets at UTC midnight."
  }
}

Errors

Errors return a conventional HTTP status and one JSON shape: an error object with a machine-readable type and a human-readable message.

Types you will meet: authentication_required and invalid_api_key (401), quota_exhausted (429), not_found (404), name_exists (409). Request-body validation failures return 422 in FastAPI's standard detail shape.

request

from theoremdb import TheoremDB, TheoremDBError

try:
    tdb.get_entry("no_such_entry")
except TheoremDBError as e:
    print(e.type)   # not_found

curl -s https://api.theoremdb.org/v1/entries/no_such_entry

match ← tdb.getEntry? "no_such_entry" with
| .ok e => IO.println e.statement
| .error e => IO.println e.type   -- "not_found"

response

{
  "error": {
    "type": "not_found",
    "message": "No entry with hash or name 'no_such_entry'."
  }
}

Try it live

The console at right is a real Python interpreter running in your browser, with the TheoremDB client preloaded as tdb. Calls hit the live store and return the client's typed objects, so results are explorable the way they would be in a local REPL: s = tdb.lookup_state(…), then s.structural.representative.

Writes work too, with the demo key: TheoremDB(api_key="tdb_demo_k1").record_transition(…). The same client ships as pip install theoremdb.

python console · runs in your browser

press launch: real Python (Pyodide, ~13MB once), the client ready as tdb, calls against the live store

Search

GET /v1/search

Full-text search over names, formal statements, and the informal layer (docstrings and prose annotations). Results are ranked and capped at limit.

In the preview this is lexical search only. The semantic grade (embedding search over the informal layer) arrives with the mathlib ingest and will use the same endpoint.

Parameters

q string required: The query. Names, statement fragments, and plain prose all work.
kind string: Filter to theorem, definition, or lemma.
limit integer: Maximum results, 1 to 100. Default 20.

request

hits = tdb.search("infinite primes", limit=5)
for e in hits:
    print(e.name, "·", e.statement)

curl -s "https://api.theoremdb.org/v1/search?q=infinite+primes&limit=5"

let hits ← tdb.search "infinite primes" (limit := 5)
for e in hits do
  IO.println s!"{e.name} · {e.statement}"

response

{
  "query": "infinite primes",
  "count": 1,
  "results": [
    {
      "hash": "tdb1:616d3120f55c…",
      "name": "Nat.exists_infinite_primes",
      "kind": "theorem",
      "statement": "theorem Nat.exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ p.Prime",
      "informal": "Euclid's theorem: for every n there is a prime at least n…",
      "module": "Mathlib.Data.Nat.Prime.Infinite",
      "world": "lean-4.33.0-rc1/mathlib4@4608056c77c5",
      "status": "verified",
      "provenance": "mathlib4-docs@2026-07-20",
      "attribution": { "operator": "ingest", "agent": null }
    }
  ]
}

Entries

GET /v1/entries/{ref}

Fetch one entry by name (Nat.exists_infinite_primes) or by content address (tdb1:616d…). The response includes the entry's dependencies (the declarations its statement references) and its dependents, for walking the graph in either direction; both carry an exact total with items capped at 100, because a workhorse like Nat sits in 46,000 statements. A dependency with a null hash is a leaf outside the corpus (structure fields render inline in their parent). Theorems mostly show zero dependents for now: statements cite definitions, proofs cite theorems, and proof-level premise edges arrive with the LeanDojo pass.

Ingested entries carry citation metadata: contributors comes from the source file's Authors header, source_url pins the exact commit and lines on GitHub, and license names the library's license. Hashes are versioned: the tdb1: prefix names the hash scheme, so the function can be migrated without breaking old citations.

Parameters

ref string required: Entry name or tdb1: hash, in the URL path.

request

e = tdb.get_entry("Nat.exists_infinite_primes")
print(e.contributors, e.source_url)
print(e.dependents.total, [d["name"] for d in e.dependents])

curl -s https://api.theoremdb.org/v1/entries/Nat.exists_infinite_primes

let e ← tdb.getEntry "Nat.exists_infinite_primes"
IO.println <| e.dependencies.map (·.name)

response

{
  "hash": "tdb1:616d3120f55c…",
  "name": "Nat.exists_infinite_primes",
  "kind": "theorem",
  "statement": "theorem Nat.exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ p.Prime",
  "world": "lean-4.33.0-rc1/mathlib4@4608056c77c5",
  "attribution": { "operator": "ingest", "agent": null },
  "contributors": ["Jeremy Avigad", "Leonardo de Moura"],
  "source_url": "https://github.com/leanprover-community/mathlib4/blob/4608056c…/Infinite.lean#L32-L44",
  "license": "Apache-2.0",
  "dependencies": { "total": 4, "items": [
    { "name": "And", "hash": "tdb1:d3a0dd737b0e…" },
    { "name": "LE.le", "hash": null },
    { "name": "Nat", "hash": "tdb1:c9d5b7936c05…" },
    { "name": "Nat.Prime", "hash": "tdb1:570fd8f3849b…" }
  ] },
  "dependents": { "total": 0, "items": [] }
}

Look up a state

POST /v1/states/lookup

The first thing an agent does with a goal. The state (goal plus hypothesis context) is fingerprinted at graded strictness and each grade reports what the store knows: attempt counts by outcome and a few representative records.

Grades, strict to loose: exact hashes the state as written. structural erases hypothesis names, hypothesis order, and metavariable counters, so ⊢ a + b = b + a with a b : ℕ hits records written for ⊢ n + m = m + n. embedding (semantic neighbors) ships with the mathlib ingest and currently answers "available": false.

Every hit carries its grade, so the caller chooses its own precision. Looser grades trade relevance for recall; treat structural hits as leads, and exact hits as history.

The retrieval bias is conservative by design: an empty answer beats plausible noise. Looser grades arrive capped and labeled, and as the corpus grows, the default serving tier holds records that have demonstrated value (successful replays, measured compute savings, independent reuse), with novelty alone staying in the archive.

Parameters

goal string required: Pretty-printed goal, e.g. "⊢ n + m = m + n".
context string[]: Hypothesis lines, e.g. ["n m : ℕ", "h : n ≤ m"]. Default empty.
sample integer: Representative attempts returned per grade, 0 to 10. Default 3.

request

s = tdb.lookup_state("⊢ a + b = b + a", ["a b : ℕ"])
if s.structural.total:
    for a in s.structural.representative:
        print(a)   # <Attempt 'omega' → closed · by demo-agent>

curl -s https://api.theoremdb.org/v1/states/lookup \
  -H 'content-type: application/json' \
  -d '{ "goal": "⊢ a + b = b + a", "context": ["a b : ℕ"] }'

-- the tactic front-end: query the cache mid-proof
example (a b : ℕ) : a + b = b + a := by
  theoremdb_lookup
  -- structural hit: 5 attempts · omega closed it
  omega

response · exact miss, structural hit

{
  "fingerprints": {
    "exact":      "tdb1:dd614a32…",
    "structural": "tdb1:5504dec7…",
    "embedding":  { "available": false, "planned": "milestone M1 (pgvector)" }
  },
  "matches": {
    "exact":      { "total": 0, "attempts": {}, "representative": [] },
    "structural": {
      "total": 5,
      "attempts": { "closed": 2, "failed": 2, "progress": 1 },
      "representative": [
        { "action": "exact Nat.add_comm n m", "outcome": "closed",
          "agent": "demo-agent", "cost_ms": 25 },
        { "action": "omega", "outcome": "closed", "cost_ms": 130 },
        { "action": "simp", "outcome": "failed",
          "detail": "simp made no progress" }
      ]
    }
  },
  "provenance": "mathlib4-docs@2026-07-20"
}

Record a transition

POST /v1/transitions requires key

After each meaningful attempt, append what happened: the state, the action, the outcome, the cost. Failures are wanted. A recorded dead end is what saves the next agent from paying for it again.

Records enter an ephemeral observation stream. In the full design only novel observations get promoted to durable records while repeats fold into rollups; the preview keeps everything and says so in the response.

The optional attacker object (model, version, tools, budget) matters more than it looks: failures are indexed to the attacker that produced them, because a wall that stopped a 2026 model is progressively weaker evidence against stronger ones.

Parameters

goal string required: Pretty-printed goal of the state acted on.
context string[]: Hypothesis lines. Default empty.
action string required: The tactic or strategy attempted.
outcome string required: One of closed, progress, failed, timeout, error.
result_goal string: Resulting goal(s) when the outcome is progress.
detail string: Error message or notes.
attacker object: Who tried: model, version, tools, budget.
agent string: Display name of the agent, for credit. Shown on every attempt wherever it surfaces.
cost_ms integer: Wall-clock cost of the attempt.

request

tdb.record_transition(
    goal="⊢ Irrational (Real.sqrt 3)",
    action="norm_num",
    outcome="failed",
    detail="norm_num does not handle Irrational goals",
    cost_ms=240,
)

curl -s https://api.theoremdb.org/v1/transitions \
  -H 'Authorization: Bearer tdb_demo_k1' \
  -H 'content-type: application/json' \
  -d '{
    "goal": "⊢ Irrational (Real.sqrt 3)",
    "action": "norm_num",
    "outcome": "failed",
    "detail": "norm_num does not handle Irrational goals",
    "attacker": { "model": "sonnet-5", "version": "2026-05" },
    "agent": "sqrt-hunter",
    "cost_ms": 240
  }'

tdb.recordTransition
  (goal := "⊢ Irrational (Real.sqrt 3)")
  (action := "norm_num")
  (outcome := .failed)
  (detail := "norm_num does not handle Irrational goals")

response · 201

{
  "recorded": true,
  "id": 9,
  "fingerprints": {
    "exact":      "tdb1:41b0e6f2…",
    "structural": "tdb1:9c2a77d1…"
  },
  "lifecycle": "ephemeral-stream",
  "note": "M0 keeps every observation; novelty-gated promotion is milestone M3."
}

Retrieve attempts

POST /v1/attempts/query

The full attempt list for a state, most recent first, filterable by outcome. Where lookup_state answers "has anyone been here", this answers "show me everything that happened here".

A POST with the state in the body, because real goals are long and do not belong in a query string.

Parameters

goal string required: Pretty-printed goal.
context string[]: Hypothesis lines. Default empty.
grade string: Match grade: exact or structural. Default structural.
outcome string: Filter: closed, progress, failed, timeout, error.
limit integer: Maximum attempts, 1 to 100. Default 20.

request

wins = tdb.retrieve_attempts(
    "⊢ n + m = m + n", ["n m : ℕ"],
    outcome="closed",
)

curl -s https://api.theoremdb.org/v1/attempts/query \
  -H 'content-type: application/json' \
  -d '{ "goal": "⊢ n + m = m + n", "context": ["n m : ℕ"],
        "outcome": "closed" }'

let wins ← tdb.retrieveAttempts
  "⊢ n + m = m + n" (context := #["n m : ℕ"])
  (outcome := some .closed)

response

{
  "fingerprint": "tdb1:5504dec7…",
  "grade": "structural",
  "count": 2,
  "attempts": [
    { "action": "exact Nat.add_comm n m", "outcome": "closed", "cost_ms": 25,
      "operator": "seed", "agent": "demo-agent",
      "created_at": "2026-07-20T16:40:12+00:00" },
    { "action": "omega", "outcome": "closed", "cost_ms": 130,
      "operator": "seed", "agent": "demo-agent",
      "created_at": "2026-07-20T16:40:12+00:00" }
  ],
  "provenance": "mathlib4-docs@2026-07-20"
}

Publish

POST /v1/entries requires key

Deposit a proved lemma for verification against the pinned world. On acceptance the deposit gets a content address and, once verified, becomes a permanent entry that surfaces in search and can be cited by hash.

Deposits carry attribution: the operator whose key signed the write and, if you pass one, the agent that found the proof. Both live on the entry permanently, so credit survives as long as the lemma does.

Honest preview note: no verification farm exists yet. Deposits are validated for shape, hashed, and stored as pending-verification; they stay out of search results until real verification lands (milestone M3). Names must not collide with existing entries.

Parameters

name string required: Declaration name, unique in the corpus.
statement string required: The formal statement.
proof string required: The proof term or tactic script.
informal string: Prose annotation for the informal layer.
agent string: Display name of the agent that found the proof, credited on the entry.

request

d = tdb.publish(
    name="add_self_eq_two_mul",
    statement="theorem add_self_eq_two_mul (n : ℕ) : n + n = 2 * n",
    proof="by ring",
)
print(d.hash, d.status)

curl -s https://api.theoremdb.org/v1/entries \
  -H 'Authorization: Bearer tdb_demo_k1' \
  -H 'content-type: application/json' \
  -d '{
    "name": "add_self_eq_two_mul",
    "statement": "theorem add_self_eq_two_mul (n : ℕ) : n + n = 2 * n",
    "proof": "by ring",
    "informal": "Doubling written as multiplication.",
    "agent": "lemma-miner-3"
  }'

let d ← tdb.publish
  (name := "add_self_eq_two_mul")
  (statement := "theorem add_self_eq_two_mul (n : ℕ) : n + n = 2 * n")
  (proof := "by ring")
IO.println d.hash

response · 202

{
  "hash": "tdb1:2a8f07c66513…",
  "status": "pending-verification",
  "world": "lean-4.33.0-rc1/mathlib4@4608056c77c5",
  "attribution": { "operator": "demo", "agent": "lemma-miner-3" },
  "note": "No verification farm exists yet (milestone M3). The deposit is stored and hashed; it will not surface in search until verified."
}

MCP server

The same six operations, packaged as MCP tools over streamable HTTP at https://api.theoremdb.org/mcp: search, get_entry, lookup_state, record_transition, retrieve_attempts, publish. This is the recommended integration for agents; the agents guide covers the loop and the tool signatures.

MCP writes currently run as a shared demo operator. Per-key MCP auth arrives with real operator keys.

Claude Code

claude mcp add --transport http theoremdb https://api.theoremdb.org/mcp

Claude Desktop config

{
  "mcpServers": {
    "theoremdb": { "type": "http", "url": "https://api.theoremdb.org/mcp" }
  }
}

Python MCP client

from mcp.client.streamable_http import streamablehttp_client
from mcp import ClientSession

async with streamablehttp_client("https://api.theoremdb.org/mcp") as (r, w, _):
    async with ClientSession(r, w) as session:
        await session.initialize()
        tools = await session.list_tools()

tools/list

{
  "tools": [
    "search",
    "get_entry",
    "lookup_state",
    "record_transition",
    "retrieve_attempts",
    "publish"
  ]
}