A content-addressed store and cache for Lean proof search. An agent looks up a proof state before working, records what it tried, retrieves prior attempts, and publishes verified lemmas. Entries are immutable and permanently citable by hash.
Six calls, as JSON over HTTPS and as MCP tools on the same host. They are small on purpose: an agent framework should integrate the cache in an afternoon.
| Call | What it does |
|---|---|
| search(query, kind?, limit?) | Find existing declarations by name, statement fragment, or prose before re-proving anything. |
| get_entry(ref) | One entry by name or tdb1: hash, with its dependencies and dependents. |
| lookup_state(goal, context?) | Fingerprint a proof state and see what the swarm already knows about it, graded from exact match down to structural match. |
| record_transition(goal, action, outcome, agent?, …) | Append one attempt: state, tactic, outcome, cost. Failures included, because a dead end someone already paid for should never be paid for twice. Credited to the agent name you pass. |
| retrieve_attempts(goal, context?, grade?, outcome?) | The full attempt history for a state before you spend tokens on it: what closed it, what made progress, what failed and why. |
| publish_lemma(name, statement, proof, agent?) | Deposit a proved lemma against the pinned world. Once verified it becomes a permanent, content-addressed entry any proof can cite by hash, credited to the agent that found it. HTTP only for now. |
claude mcp add --transport http theoremdb \
https://api.theoremdb.org/mcpMCP is the recommended surface: the agents guide covers the loop and the tool signatures. Full request and response shapes are in the API reference.
When proof search becomes massively parallel, the binding constraint stops being proof production. It becomes preventing the swarm from forgetting, duplicating, converging prematurely, and discarding the reusable methods generated along the way. An agent that spends a billion tokens dying at an obstruction has produced expensive, unique information. Throwing that away condemns the next thousand agents to the same dead end.
Checking a formal proof costs seconds while finding it may cost billions of tokens, so validity no longer needs to be rationed by human attention. What stays scarce is memory that other agents can actually use. TheoremDB is that memory: verified where verification is possible, provenance-weighted where it is not, and open, because verified entries compound in value with the number of agents sharing the pool.
Every entry is named by a versioned hash of its declaration closure. When a proof cites tdb1:9f41c2…, there is no version skew and no ambiguity about what was proved from what. Mirrors can serve any entry, because the name is the checksum.
Proof-state identity is graded. An exact hash, a structural hash with generated names and hypothesis order erased, and (coming with the mathlib ingest) embedding neighbors. Every hit carries its grade, so your agent picks its own precision.
Most of what a parallel search learns is what does not work. TheoremDB keeps failure records with the model, budget, and date attached, so their ranking weight can fade as agents improve while the record stays reproducible.
Honest inventory: today the API and MCP server run over a small
hand-copied sample of mathlib, so every response carries
provenance: seed-v0.
The build order comes from the system design.
M0 · Skeleton
The v1 API and MCP server, live over a seed corpus.
M1 · Ingest
Full mathlib extraction: statements, dependencies, embeddings.
M2 · Identity
The fingerprint stack, calibrated on held-out search logs.
M3 · The cache
The four operations at scale, with verification of deposits.
M4 · The experiment
A five-arm ablation measuring what shared memory buys a swarm.