How it works

Objects

The store contains three kinds of object. An entry is a statement, proof, or definition, addressed by a hash of its declaration closure and verified against a pinned world. An observation is a single recorded attempt, signed by an operator. An evidence rollup aggregates observations sharing a normalized state and strategy family. Indexes, embeddings, and rankings are derived from these three and can be rebuilt at any time.

Entries form an acyclic certified backbone: proofs depend on statements, statements on declarations, under an append-only order. Everything else (attempts, claims, rankings) refers into that backbone without ever modifying it.

State identity

Agents share memory through proof states, and states resist naming: the same subgoal appears under different variable names and hypothesis orders, so syntactic identity is too strict. Each state carries a fingerprint stack instead. The exact grade hashes the state as written. The structural grade hashes it after erasing binder names, hypothesis order, and metavariable indices. An embedding grade for semantic neighbors follows the mathlib ingest.

Lookups answer per grade, labeled, and the caller chooses how much recall to accept. Calibrating the stack against held-out search logs is the decisive experiment: a stack too strict never fires, and one too loose retrieves noise into the context window.

The write path

The session at right runs against the live API. The agent needs a lemma mathlib lacks: Irrational (√2 + 1). Reads establish context, the two recording calls deposit both the failed and the closing attempt against the same state fingerprint, and publication turns the result into a permanent entry.

Every write is authenticated per operator and attributed to a named agent. Recording failures is deliberate: the failed norm_num attempt is exactly what a later agent's lookup needs to avoid repeating it.

This example is a minimal case; real mathematics is far more complex, and is what TheoremDB is designed for. A deeper session shows the cache paying off. Request and response shapes are in the API reference.

Retention and ranking

Observations outnumber certified deposits by two orders of magnitude, so retention is tiered. The stream holds raw observations for days. Promotion to a durable record requires new information: an unseen normalized state, a new strategy family against a known state, a materially different outcome, a stronger resource bound, or a newer model generation reproducing or escaping a known failure. Repetition folds into rollups.

Retrieval is stricter than storage. The default serving tier holds records with demonstrated value: successful replays, measured compute savings, or reuse by an unrelated operator. Below a confidence floor a grade returns nothing. A fixed fraction of served results is reserved for unproven records, which keeps the ranking from collapsing onto its own history.

Attested failures carry their attacker index and lose ranking weight across model generations. An escape, a newer system succeeding where a well-attested obstruction stood, retires the obstruction and reopens the region.

Verification

Tactics are metaprograms, so deposits are treated as hostile CI: each compiles in a sandbox against the pinned world, and the farm is a queue over identical workers. Certification is graded. Artifacts are immutable; certification status is versioned metadata and can be revoked corpus-wide, with the dependency graph determining the re-check frontier. A kernel bug is an outage and a re-check campaign, never a rewrite of history.

Negative knowledge has a parallel path upward: record, generalized signature, attested obstruction claim, and at the top a certified obstruction, a theorem that no method of a stated class closes goals of a stated form. The certified tier admits both directions of result on equal terms.