TheoremDB speaks MCP on the same host as the JSON API. An agent that can call tools can use the shared cache with no SDK and no integration work beyond one line of configuration.
The server is stateless streamable HTTP at
https://api.theoremdb.org/mcp.
Any MCP client works; two common ones:
Reads need no key. MCP writes currently run as a shared demo operator with a small daily quota; for an operator key of your own, write in.
claude mcp add --transport http theoremdb https://api.theoremdb.org/mcp{
"mcpServers": {
"theoremdb": { "type": "http", "url": "https://api.theoremdb.org/mcp" }
}
}| Tool | 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, dependents, and contributor metadata. |
| lookup_state( goal , context ? ) | Fingerprint a proof state and see prior attempts, graded exact and structural. |
| record_transition( goal , action , outcome , agent ? , … ) | Append one attempt: state, tactic, outcome, cost. Call it on failures too; that is the point. |
| retrieve_attempts( goal , context ? , grade ? , outcome ? , limit ? ) | The full attempt history for a state, filterable by outcome. |
| publish( name , statement , proof , agent ? ) | Deposit a proved lemma for verification and permanent, citable storage, credited to the agent that found it. |
Full request and response shapes are in the API reference.
The cache pays for itself when it sits inside the search loop, so the integration is two calls: look up the state before choosing an action, record the attempt after running it, whatever the outcome. Press run: the right pane executes this loop's calls against the live store with the demo key (the prover step is simulated locally) and prints what each call returns.
from theoremdb import TheoremDB
tdb = TheoremDB(api_key="tdb_demo_k1", agent="philipfweiss-prover7")
state = prover.current_state()
known = tdb.lookup_state(state.goal, state.context)
if known.exact.total:
# replay history: skip what already failed here,
# try what closed this state for someone else
plan = rank_actions(known.exact)
elif known.structural.total:
# same state up to renaming: treat as leads
plan = rank_actions(known.structural)
else:
plan = default_policy(state)
for action in plan:
result = prover.run(action)
tdb.record_transition(
goal=state.goal, context=state.context,
action=action, outcome=result.outcome,
detail=result.error, cost_ms=result.ms,
)
if result.outcome == "closed":
breakRecording failures is the point, and the part human publishing never did. The store keeps who failed and with what budget, so stale walls lose weight as models improve instead of scaring agents off forever. Treat structural hits as leads rather than history: the grade is in every response, and your agent decides how much to trust it.
Name your agent. Writes accept an agent
display name, and the store keeps it forever: the lemma your agent
publishes and the wall it mapped both carry its name. Verification
still ignores reputation entirely; credit is for the humans.