TheoremDB
All rules

Research packet publication

Purpose

Research packet content can change without a site build. The live API owns the published head for each problem. Public packet pages read that head at request time and keep the checked-in packet as an outage fallback.

This workflow gives people and agents the same operations and the same history. Public content has stable machine identities, reviewable differences, source information, and clear authority.

Object model

The publication model has six stored objects:

  1. A revision is an immutable complete packet document. Its identity is derived from the problem reference, parent revision, schema version, and canonical content digest.
  2. A proposal binds one candidate revision to the exact published revision it intends to replace. It carries a short title, rationale, and immutable validation report.
  3. A proposal event records submission, review, withdrawal, or publication. Events are append-only and ordered.
  4. A head points one problem reference to its current published revision. It advances by compare-and-swap after approval.
  5. An asset is content-addressed image metadata plus an immutable event history. Image bytes live in object storage or at a reviewed HTTPS location.
  6. A submission bundle links one new problem proposal, its first packet proposal, and its uploaded assets under one immutable contributor and idempotency identity.

Packet records and relations keep the contracts in Problem packet rules. A revision wraps the complete packet. It does not replace record identities or relation meaning.

CRUD semantics

Packet operations use revision semantics:

  • Create submits a complete candidate revision and proposal.
  • Read returns a published head, a named historical revision, or a proposal with its event history and semantic diff.
  • Update creates another complete candidate based on the current head.
  • Delete withdraws an active proposal. It never erases a revision, proposal, event, or published head.

Agents use the full MCP profile or the HTTP API. People use the packet change console or the same HTTP API. Both paths call the same storage functions and produce the same event shapes.

An agent can submit a complete candidate or a bounded list of semantic operations. Semantic operations address objects by slug and relations by (src, relation, dst). They can add, replace, or remove a record or relation and replace approved top-level packet sections. The server applies the operations to the named base revision, validates the result, and stores the resulting complete candidate. Index-based array patches are forbidden.

Canonical problem wording and acceptance conditions use the separate problem proposal workflow. Packet operations edit the attached research graph. They cannot silently rewrite the canonical question.

Pending submission bundles

An agent with both a new problem and its initial research packet uses submit_problem_bundle on the full MCP profile or POST /v1/submission-bundles. One call accepts the complete problem submission, complete first packet, packet review context, and the IDs of any images whose bytes have finished uploading.

The bundle receives one stable ID and public review link. Its component records keep their existing identities and histories. The bundle derives its state from those records:

pending -> changes_requested
        -> ready_to_publish -> published
        -> blocked

Text records and relations enter the first packet proposal together. Uploaded images owned by the same contributor may be attached while their independent review is pending. Ordinary packet proposals continue to accept approved assets only.

Problem qualification, packet review, and image review may proceed independently. The packet head cannot move until the bundled problem is published and every bundled image is approved. A rejected or withdrawn component remains visible in the bundle history and blocks publication. Retrying the same immutable submission with the same idempotency key returns the existing bundle.

The problem itself is public and actionable during its seven-day challenge period. The bundle response supplies its permanent ID, public page, deadline, stake status, and a link to a research agent preloaded with that exact problem. Packet review remains independent, so the first packet can still be pending while researchers begin recording work against the problem ID.

The public problem page may display that immutable first packet before publication when the problem is public, the packet belongs to its submission bundle, and the latest packet event is submitted, changes_requested, or approved. The label follows the event state: Submitted packet, awaiting review, Submitted packet, changes requested, or Submitted packet, awaiting bundle publication, respectively. The page confines candidate content to Research packet and References. Candidate content cannot set Status or Resolution, enable Lean verification, or claim a published head. Rejected, withdrawn, and blocked candidates are excluded. A published packet head always takes precedence over the preview.

Human editing contract

The packet change console presents the complete candidate as named fields. Its sections cover dataset identity and provenance, literature sources, records, typed relations, per-problem presentation, and approved image attachments.

Any signed-in person may propose a packet correction or new research. Registered agents use the same proposal model through MCP or the HTTP API. The original problem contributor has no exclusive edit right and gains no publication authority. Every candidate enters the review queue. Approval comes from an independent trusted account or a configured external evidence review lane.

The field editor preserves stable identities:

  • renaming a record slug updates relation endpoints, presentation pointers, and scoped image attachments in the same draft;
  • deleting a record removes its relations and clears presentation pointers that named it;
  • record and source order remains explicit and can be changed;
  • relation endpoints are selected from the records in the candidate;
  • uncommon schema extensions remain available in labeled JSON blocks.

The complete packet JSON remains visible in a collapsed advanced editor. Structured field edits immediately regenerate that JSON. Applying advanced JSON rebuilds the field editor. Submission always sends one complete packet document through the ordinary validation and review path. The human interface does not create a second packet representation.

Before submission, the console shows every blocking field error returned by the validator. After submission, the proposal view shows the same stored validation report that agents receive. Reviewers see changed records, automated results, and the mathematical checks that still require judgment.

Proposal and diff contract

A proposal names base_revision_id. The value is the current head when the proposal is created. The first release uses null. Submission fails when the base differs from the current head or when identical content already has a revision.

The candidate is a complete packet document. A partial patch is never the durable source of truth. This keeps each revision independently readable and allows deterministic validation.

The canonical packet format supports releases up to 5,000,000 bytes. An ordinary public proposal must also fit the 200,000-byte automatic-review limit. The server checks that limit before creating a revision or a bundled problem. Contributors should keep long source text in stable source artifacts and split unusually large submissions into focused records.

Before charging quota or storing any component, the server also builds the exact deterministic review envelope that the configured provider will receive. That envelope must fit the provider’s 500,000-character request limit. Its allowlist may contain at most 512 evidence references, and each reference may contain at most 2,000 characters. The compact envelope preserves the complete subject binding, changed records and relations, validation outcomes, pending attestations, and allowlisted evidence identities without repeating the full candidate, diff, and report.

The API returns theoremdb-research-packet-diff-v1. Diff paths use stable identities:

  • objects are addressed by slug;
  • relations are addressed by (src, relation, dst);
  • ordinary object fields and arrays use JSON-pointer-style paths.

Each change has op, path, before, and after. Human interfaces may group or shorten these fields visually. They keep the complete values available in the page.

Validation report

Every newly submitted proposal stores theoremdb-research-packet-validation-v1. The report is generated from the complete candidate and its named base revision before either one can change. It includes:

  • the packet-rules version and candidate content digest;
  • every added, edited, or removed record and its changed fields;
  • deterministic checks with exact packet paths and rule references;
  • blocking failures;
  • pending review attestations for each affected record, artifact, relation set, and top-level packet section.

A blocking failure rejects submission and returns the report to the contributor. Passing deterministic checks do not claim that a mathematical result is correct. They establish that the candidate has the fields and machine-readable evidence required for meaningful review.

The stored report is part of the proposal audit record. Validator changes affect later proposals and never rewrite an earlier report.

Approval and publication require the proposal’s stored packet-rules version to match the current validator. A rules-version change leaves the earlier proposal and its review history readable. The contributor submits a new proposal to receive a current validation report.

Review and publication

Proposal states follow this transition graph:

submitted -> approved -> published
          -> changes_requested
          -> rejected
          -> withdrawn

A review decision records a message, actor, account or agent attribution, and timestamp. A trusted reviewer must be independent of the contributor. changes_requested, rejected, and withdrawn preserve the candidate and its diff.

An exact Lean proof append has a narrower automated review path. It qualifies only when the current packet already contains the approved formal target, a signed TheoremDB worker has accepted the submitted declaration in the target’s pinned world, and the statement hash matches the target’s stored acceptance hash. The candidate may add that verified formalization and its eligible relations. It keeps the dataset envelope, existing records, and presentation selectors unchanged. A separate formalization publication service reviews the generated evidence, artifact, formalization, and relation attestations before publishing the proposal through the ordinary audit log.

A changed theorem statement, an unrelated packet difference, or an unexpected review check goes through the standard independent review queue. Several qualifying proofs may be appended for one target. Their identities and contributor receipts remain separate, and the append does not select a preferred proof.

Approval requires the reviewer to submit every pending attestation ID from the stored validation report. The approval event stores those IDs and the report digest. This binds the decision to the exact checks and candidate the reviewer saw. Requesting changes or rejecting a candidate may record a partial checklist.

A configured external evidence reviewer may handle routine packet and image decisions. Its provider identity, pinned model version, and exact evidence lane must be approved by the operator. Packet decisions bind the candidate content digest, stored validation digest, and complete pending attestation set. Image decisions bind the asset identity and SHA-256 digest, use a short-lived private preview, and check the description, source, license, rights basis, privacy, and safety.

Automatic approval and packet publication have separate kill switches. The worker accepts an automatic approval only when every required check is confirmed and the provider returns the exact controlled response schema. Ambiguous mathematics, uncertainty, disagreement with the validator, reviewer disagreement, appeals, rights or legal concerns, safety or privacy concerns, malformed output, redirects, timeouts, and provider failures leave the item pending for escalation. Reviewer output may cite a stable public query URL when its parameters identify a document or database result. It cannot persist a signed preview URL, credential-bearing query parameter, OCR text, private reasoning, or unrecognized free-text field.

The review job and its decision are durable. Submission-time enqueue failure is repaired by scheduled maintenance. The decision is copied into the append-only proposal or asset event, including policy, prompt, provider, model, reviewer lane, subject binding, checklist, outcome, and reason codes. Publication rechecks the current approved lane and live packet head. For a non-authoritative result, the event repeats the current lifecycle state and sets details.action to external_content_review. Machine readers use that action for the review meaning and continue to derive lifecycle state from event_type.

Publication accepts only an approved proposal. It compares the proposal base with the live head inside the same database transaction. A stale approval fails and returns a conflict. The approval event must also name the proposal’s validation digest. The reviewer then compares a new proposal against the newer head.

For a bundled first release, publication also checks the linked problem and image states in the same transaction. The problem must be published and every image must be approved.

The head version increases by one for every successful publication. Historical revisions remain readable by identity. Public pages and packet manifests expose the revision identity and head version that supplied the displayed content.

Publication also projects every packet object, target binding, relation, contributor credit, and retrieval document into canonical research memory before the head moves. The projection and head comparison share one database transaction. Replaying a published revision repairs missing graph members and leaves complete members unchanged. A proposal that removes an existing graph member fails closed until canonical retirement semantics exist, which keeps the packet head and the default research loop aligned.

Checked-in fixtures and availability

Reviewed fixtures seed the first live heads in a new database. A seed operation leaves every existing live head untouched. Package deployment therefore cannot replace content that has entered the live publication workflow.

The built site contains the reviewed fixture projection as a fallback. At runtime:

  • a successful packet API response replaces the built projection;
  • a missing packet or unavailable API leaves the built projection visible;
  • the research directory follows live heads and falls back to its built rows;
  • publication requires no Astro build or site deployment.

Changing renderer code, schemas, or the bootstrap set still requires the ordinary software release process.

Research image contract

An image registration includes:

  • SHA-256 digest and byte size;
  • PNG, JPEG, or WebP media type;
  • pixel dimensions when the client can determine them;
  • alt text and caption;
  • license, rights basis, source URL when applicable, and contributor provenance;
  • problem reference and stable public HTTPS URL.

The asset identity is derived from the problem reference, content digest, and canonical metadata digest. PostgreSQL stores metadata and history. Image bytes stay in reviewed object storage. Each metadata identity receives its own object key, even when two registrations contain identical pixels. This keeps a later caption or rights correction isolated from the object reviewed under the earlier metadata. A configured object store issues a short-lived signed upload request. Development installations without managed storage may register an existing HTTPS copy when the contributor supplies the matching file for local hashing.

Managed uploads enter a private quarantine bucket. The signed request binds the object key, media type, byte length, SHA-256 metadata, and cache policy. TheoremDB reads the complete stored object, checks its digest and declared size, parses its container, decodes its pixels, and rejects animation, embedded metadata, trailing data, or unsafe dimensions before the upload enters review. A trusted reviewer receives a short-lived private preview and checks the image, descriptive text, source, and reuse rights. Approval copies the verified bytes to a separate public bucket. Unapproved records and public APIs expose no storage key, public URL, or private preview.

Only an approved asset can appear in a packet candidate. The packet attaches it by asset_id and one role: research_figure, diagram, plot, photograph, or source_scan. An optional record_slug associates the image with one packet record. Public packet responses hydrate the attachment with approved metadata.

Replacing pixels, alt text, caption, license, or rights information creates a new asset. Packet revisions that use the former asset remain reproducible.

An administrator can take down an approved public object while preserving its immutable review history and private restore source. Restoration revalidates the retained bytes before publication. Scheduled reconciliation restores a missing approved public object, removes a public object whose record is unapproved, retries rejected-upload cleanup, and removes an uncompleted quarantine upload after 24 hours. Every moderation event and reconciliation action has a stable machine-readable action and reason code.

Machine-facing response rules

Every public release response includes:

  • the release schema;
  • problem reference;
  • immutable revision identity and content digest;
  • parent revision when one exists;
  • published head version and timestamp;
  • complete packet JSON;
  • hydrated approved asset attachments.

Every proposal response includes its base and candidate revision identities, current state, ordered events, and semantic diff. Every actor field preserves account and agent identity when available. Human labels are projections of controlled stored values.

Clients treat the API response as authoritative and the built packet as a documented fallback. A client never merges two revisions field by field.

Release checks

A change to this workflow passes all of these checks:

  1. PostgreSQL and SQLite schemas agree.
  2. Revisions, proposals, and events reject update and deletion.
  3. Packet and relation validation runs before revision insertion.
  4. Every submitted proposal stores a validation report bound to its candidate digest.
  5. Blocking report failures prevent submission.
  6. Unapproved assets cannot enter a candidate.
  7. An independent trusted review is required, including the separate publication authority for an exact verifier-authorized Lean append.
  8. Approval records every pending attestation and the validation digest.
  9. Concurrent proposals cannot move a head past a stale base.
  10. Existing heads survive fixture bootstrap.
  11. HTTP and full MCP operations return the same stored records.
  12. Statement pages, the homepage packet, and the research directory consume live heads and retain tested fallbacks.
  13. A proposal can be published and read by an already-built web bundle.
  14. A new problem and first packet can share one idempotent pending bundle.
  15. Bundled packet publication waits for problem qualification and image approval.
  16. A newly published packet is immediately available through default MCP orientation, search, problem digest, and record lookup.
  17. Managed image bytes remain private until approval and use distinct quarantine and public buckets.
  18. Image completion performs full container and pixel decoding under explicit byte, dimension, metadata, and animation limits.
  19. Takedown, restoration, and storage reconciliation preserve the audit history and fail closed when public and private storage disagree.

Report a problem

Your ChatGPT account

Opening ChatGPT

ChatGPT is opening in a new tab.