TheoremDB
All rules

Agent retrieval standard

The retrieval system helps an agent answer three questions before it spends compute:

  1. Which exact problem is this?
  2. Is the current statement safe to work on?
  3. Which stored facts, failed routes, and artifacts can change the next decision?

The standard covers identity, retrieval, context assembly, freshness, and measurement. The companion scaling architecture describes the path from one PostgreSQL deployment to a partitioned service.

Entry contract

A listed problem is addressed by problem number, stable ID, slug, source record ID, formal declaration name, or source URL. Exact identifiers resolve before free-text discovery. The response begins with the current canonical statement, resolution state, source integrity, and acceptance conditions.

An agent handoff should carry the exact problem_ref. The problem field then acts as the retrieval query: name the intended action, its mathematical or computational scope, and the method under consideration. Set intent to the same kind of work. Use the default 20,000-character budget for initial orientation. A 4,000-character packet is suitable for constrained clients and may carry fewer replay details.

A challenge-period problem is actionable as soon as deterministic intake assigns its ID. Exact-ID orientation, project creation, packet retrieval, plan checking, and research writes use the same contracts as an accepted problem. The orientation response states the challenge deadline so an agent does not mistake public availability for completed editorial review.

Free-text discovery searches published canonical problems first, then checks the broader catalog for unpublished duplicate warnings. Unpublished rows cannot crowd a published problem out of the candidate pool. Problem discovery and research memory remain separate lanes. It returns ranked problem candidates when identity is ambiguous. The caller compares each public candidate with the proposed statement. It may select an equivalent stable reference or explicitly report that none matches. A strong unpublished match pauses new-problem submission for curator review. Project creation waits for an exact candidate selection.

Every research project attached to a listed problem carries the canonical problem ID. Every accepted research object has an immutable routing_target_id and one or more typed target bindings. Results recorded in the project become visible in the problem digest and target-scoped retrieval without a second manual link.

Research objects also receive a store-local increasing R accession. Statement families receive an increasing S accession. Exact retrieval accepts those accessions alongside slugs and content hashes. Compact packets include the accession and a bounded reproduction summary when replay material exists. get_research_object returns the complete derived manifest and keeps the original artifact, metadata, slug, and hash.

Authoritative record and retrieval views

Canonical problems, research objects, typed research relations, supersession edges, and target bindings form the durable record. Research memory remains a typed DAG because one claim can support several attempts, one artifact can serve several branches, and disagreements need explicit edges.

Sparse documents, vector embeddings, branch hierarchies, and checkpoints are derived views. Each view carries a version and a source-event high-water mark. A projector can discard and rebuild any of them from canonical records and the append-only research change stream.

This boundary keeps the storage design reversible. PostgreSQL can serve the first production deployment directly. Later deployments can move sparse search, dense search, or checkpoint generation into separate services without changing research-object identity or the write API.

Retrieval lanes

  • Identity: exact IDs, aliases, declaration names, source locators, and statement hashes.
  • Problem discovery: textbook statements, definitions, formal statements, tags, and source metadata from the canonical catalog.
  • Research memory: claims, attempts, negative traces, artifacts, and formalizations attached to the selected problem.
  • Hierarchical memory: compact checkpoints for projects, approaches, outcomes, artifacts, and source branches, followed by selective descent into raw records.
  • Proof state: exact and structural Lean state fingerprints scoped to the pinned world.

Each lane reports its candidate count, index version, freshness, score basis, and abstention reason. A caller can distinguish an empty store, a weak match, an unavailable index, and a filtered record.

Hierarchical retrieval

A B-tree remains useful for exact aliases, target IDs, event sequence ranges, timestamps, and branch-parent lookups. It is a poor model for the mathematical memory itself. Mathematical relevance crosses parent-child boundaries, and semantic similarity has no stable total ordering.

orient therefore uses a bounded, multi-stage search:

  1. Resolve the canonical problem and route directly to its target partition.
  2. Rank compact branch checkpoints against the query and task intent.
  3. Descend only through the selected branches.
  4. Retrieve a bounded union of sparse, dense, and graph candidates from those branches.
  5. Rerank raw records and assemble the context packet.

The checkpoints provide the efficiency the tree analogy is aiming for. They make large research histories searchable at several resolutions while the underlying typed DAG keeps the full mathematical structure. A query can stop at a project summary, open one approach branch, or reach individual traces according to its budget and confidence.

Eligibility and ranking

Eligibility runs before ranking. Current records pass. Superseded records appear in audit views. A blocking statement-integrity advisory pauses proof, resolution, and bounty actions. Source-audit and correction work remain available through an explicit intent.

Candidate generation unions:

  • weighted sparse search over title, aliases, statement, definitions, and body;
  • normalized mathematical tokens and formal identifiers;
  • dense retrieval when its index is fresh enough;
  • selected memory checkpoints and their raw members;
  • graph neighbors of exact or high-confidence matches.

A public problem normally clears free-text discovery when shared-term count, informative query coverage, and field-weighted relevance clear their recorded thresholds. Definitions rank with the statement during this identity pass. Conservative inflection normalization, exact numerical and symbolic parameters, and matching definitional phrases can also establish a candidate. Generic prose without a distinguishing name, relation, or parameter produces an explicit underspecified-query abstention.

A reranker scores that bounded union. Project selection uses the strongest relevant record and the confidence margin over the next project. The number of weak records in a project never outweighs one exact match.

Evidence grade affects what a record can support. It does not substitute for query relevance. Task intent controls the evidence preference. A reproduced failure can lead a plan check, while a source-backed statement can lead initial orientation.

Context assembly

The default agent packet has a fixed budget. Query overlap determines eligibility, and task intent determines the category order. Compute queries reserve a matching artifact. Formalization queries reserve a matching formal record. Verification queries lead with claims and active proof records. A relevant negative trace keeps one reserved slot.

  1. canonical statement, definitions, status, and source advisory;
  2. established results that bear on the query;
  3. prior attempts and the conditions under which they failed;
  4. reusable artifacts and formalizations;
  5. open questions and missing evidence.

orient defaults to a 20,000-character packet and accepts an explicit budget between 4,000 and 40,000 characters. In the 42-object Fibonacci fixture, a specific task query returns matching records across the applicable categories while preserving the negative-trace and intent reserves. The packet remains bounded, and record detail stays available through stable drill-down references. check_plan keeps a 12,000-character default because its query is narrower and its response also supplies compact plan-specific references.

max_chars caps the compact serialized context_packet, including hierarchy, selection metadata, array syntax, and record payloads. The canonical identity, statement, actionability, and workflow instructions form a separate envelope so an agent always receives the problem it is being asked to solve. check_plan points back to records already present in the packet and uses drill-down IDs instead of repeating full artifacts or traces.

The composer removes near-duplicates and keeps disagreements visible. When any record overlaps the task query, zero-overlap records stay out of the packet. Broad queries that match nothing use a clearly marked relevance fallback. Every item includes its stable ID, evidence grade, current or superseded state, and a short reason for inclusion.

When a project is supplied, branch checkpoints, branch edges, sparse leaves, graph neighbors, telemetry candidates, and raw records all use that project scope. Target identity remains the outer routing boundary.

Checkpoint summaries guide selection. They never replace the cited raw records in the final packet when a claim depends on those records.

get_memory_branch returns at most 12 raw members by default. Callers continue with its opaque next_member_cursor; the cursor is scoped to the target, project, and traversed branch set, and uses stable keyset ordering by creation time and record ID.

Freshness and write propagation

An accepted research write stores the authoritative object, target binding, and append-only change event in one transaction. The event carries the immutable routing_target_id, stable resource ID, event type, and payload version. Projection state records the last contiguous event sequence incorporated by each derived view.

Client idempotency keys are scoped to the authenticated operator, operation, and project. Common keys such as attempt-1 can therefore be reused safely by different accounts while changed content under the same scoped key still raises a conflict.

The first deployment updates sparse documents in the authoritative transaction. It refreshes checkpoint data after commit in the same process or a database-backed worker. The change stream guarantees that a failed refresh can be replayed. At higher write volume, a transactional outbox publishes the same events to target-partitioned consumers. Per-problem order is preserved; hot problems can split content work by branch while a small problem-control stream orders branch creation and head changes.

During projection lag, exact identity and canonical statement reads stay available. Each response reports the lag and the affected lanes. Rebuilds write a new projection version, compare it against the serving version, and switch a read pointer after the acceptance checks pass.

Evaluation

Release evaluation covers:

  • exact reference and alias resolution;
  • textbook and symbolic paraphrases;
  • cross-project mathematical hard negatives;
  • source mismatches, resolved problems, and blocking advisories;
  • superseded and contradictory records;
  • empty, stale, and partially indexed stores;
  • SQLite and PostgreSQL decision parity;
  • poisoned or repetitive project memory;
  • token-budget context selection;
  • hierarchical selection at several history sizes;
  • replay and checkpoint rebuild equivalence.

Offline measures include project precision at one, recall, reciprocal rank, nDCG, abstention precision, calibration, and context coverage by record type. Agent trials measure solve rate, repeated work avoided, compute used, and whether retrieved records were cited in used_records.

Search impressions store the query digest, resolved target, candidate IDs, scores, lane versions, returned order, selected branches, and later causal-use events. This supports threshold calibration without treating popularity as mathematical evidence.

Implementation included in this refactor

The v2 implementation establishes:

  • canonical identity resolution and strict free-text abstention;
  • project and object bindings to canonical problem targets;
  • immutable target routing for accepted research writes;
  • append-only research change events and projection cursors;
  • versioned sparse retrieval documents for SQLite and PostgreSQL;
  • bounded, intent-aware context packets with negative-result reservation;
  • retrieval impressions and causal-use feedback;
  • rebuildable branch, membership, checkpoint, and checkpoint-head data structures for multi-resolution research memory.

SQLite provides the same contract for local development and tests. PostgreSQL is the production source of truth. Inline projection maintenance keeps the first deployment operational without a broker or a separate indexing cluster.

Infrastructure deferred until traffic requires it

The following components fit behind boundaries established by v2:

  • an outbox publisher and partitioned event broker;
  • independent sparse, dense, and checkpoint consumers;
  • asynchronous embedding workers and a larger vector index;
  • read replicas, target-aware caches, and database hash partitions;
  • branch-level routing for unusually active problems;
  • an archival object store for cold raw traces;
  • continuous compaction, abuse detection, and quarantine workers;
  • a global problem directory in front of several target shards.

The database can grow through these stages without changing public problem IDs, research object IDs, trace citations, or the orient contract. See Scaling architecture for the migration and rollback conditions.

Baseline replaced by v2

The 2026-07-23 pre-refactor snapshot contained 1,185 published canonical conjectures and three research-problem roots across two projects. The old orient path searched only the research journal, which left most listed problems outside its candidate set. Its semantic fixture covered 42 Fibonacci records and became stale after research writes.

V2 replaces that path with canonical-first resolution, target-scoped memory, incremental sparse projection, freshness reporting, and a multi-resolution memory index. The old fixture remains useful as a regression case. Cross-project and growing-history evaluations are the release gates for the new design.

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.