tb-agents

Claude Agent SDK services that run AI collaborators on TheoremBase. Two agents, each with its own site account, runnable side by side:

• Coauthor agent (Claude-agent-v1, python -m agent_service.runner) — message-driven. Receives instructions through the site's direct messages (/messages in the frontend), works on theorem and proof drafts through the REST API, invites its conversation partner as coauthor, and publishes only with that partner's explicit approval. It answers only its owner (AGENT_OWNER).
• Reviewer agent (Claude-Reviewer-v1, python -m agent_service.reviewer) — publication-driven. Watches for newly published theorem and proof versions and reviews each one: structured comment, verify (proofs only), flags for defective statements and proofs, thumbs feedback, and a DM to its owner whenever it flags something. It reviews only items its owner authored or coauthored.

Every agent works for one person, its owner (AGENT_OWNER). The coauthor agents answer only the owner, the reviewer reviews only the owner's own work, and no agent can message or edit a conversation with anyone else (enforced in tb_client.py, beneath every tool). These are personal tools, not a service for other TheoremBase users; see "Authentication and personal use".

Requires Claude, a proprietary service. tb-agents is free software (GPL v3), but it runs on Anthropic's Claude through the Claude Agent SDK and the Claude Code CLI, which are not free software. Running it needs an Anthropic account and is subject to Anthropic's terms.

Questions, bug reports and security issues: contact@theorembase.xyz. (The code forge does not accept public sign-ups, so issues cannot be filed there.)

How it works

Aaron (frontend /messages)  <-- direct messages -->  TheoremBase API
                                                          ^
                                                          | polls inbox, replies,
                                                          | drafts/validates/invites
                                                     runner.py (this repo)
                                                          |
                                                          v
                                             Claude Agent SDK (claude-opus-5)
                                             one resumable session per partner

• runner.py logs in as the agent account and polls /api/v1/messages/inbox every AGENT_POLL_SECONDS.
• Each unread message from an allowed partner is fed into a Claude Agent SDK session. The session id is persisted per partner in agent_service/state/sessions.json, so conversation context survives restarts (resume=).
• The agent has no built-in tools — only the in-process MCP tools in tools.py. The ones that shape how it works:
  • tb_api — general TheoremBase API calls. Publish/moderation endpoints are blocked here. Before a request is sent the path is normalized (/api/v1 prefix, deprecated underscore spellings, + in timestamps) and checked against the API's own OpenAPI route table (routes.py, fetched at startup): a guessed route is refused with the nearest documented ones named, instead of costing a 404 and a second guess. Error bodies carrying a detail.code get a one-line hint (the graph routes' redaction codes, the citation codes with the server's own detail.hint naming the right field, the whiteboard section codes with the pane's section list).
  • tb_publish — publish/moderation calls; requires a verbatim quote of the partner's approval message and logs it. Refuses a publish whose drafts have no summary (the workflow's checklist item the site turns into the page description).
  • tb_version_cards — the site's version card, batched: standing and supersession state, reception, redaction exposure, stale dependencies with missing clause anchors, defined anchors, and optionally proofs and dependency rows. One call where the agents used to make five or six.
  • tb_related — what exists around a concept: the site's related_to search plus the item's curated relations, so near-duplicates under different notation are found before drafting (the first project used related_to four times against 800 keyword searches).
  • tb_resolve_labels, tb_catalog (server-paged; terms=a,b,c probes every candidate name of an area in one call and answers one block per term plus the terms that matched nothing, the budget spent evenly across the groups so a truncation never loses a whole term), tb_my_drafts (proofs carry a state too, from published_versions_count, with stranded and withdrawn proofs marked), tb_get_many, tb_read_text — lookups and bounded reads.
  • tb_patch_text, tb_patch_text_many, tb_copy_proof (the site's copy-from-version, floating or pinned; the origin's summary is carried on both origin paths and its length reported), tb_refresh_dependencies (the site rewrites a draft's stale labels to the latest standing versions, on any draft including a fresh copy; the migration path is copy, refresh on the copy, validate, publish - never relabel by hand), tb_diff_draft — edits that keep stored text out of the model's context.
  • tb_relate_many — every curated relation of a publish in one POST /relations/batch call: one from -> to : kind [: note] row per edge, labels resolved first, one result line per row; a per-row 409 is reported as "already exists", never as a failure of the batch.
  • tb_send_message, the whiteboard tools, and the shared-documents reader.
  • arxiv_search, arxiv_fetch, arxiv_read — arXiv, v2 coauthor only (AGENT2_ARXIV=false turns them off). Search is arXiv's own metadata index: titles, abstracts, authors and categories, never the body of a paper, so a phrase from inside a proof matches nothing. A fetch pulls the LaTeXML HTML of one version, converts it, and returns a map - every section, theorem and proof with an anchor, a label and a line range - which is ~2-4 KB against a paper of ~150,000 characters; blocks are then read one at a time by label. Every <math> in that HTML carries the author's original LaTeX in its alttext, so quotations paste into a draft unchanged and the source tarball is never needed. Papers with no HTML rendering are refused outright; there is no fallback to ar5iv or PDF. Fetched papers are cached under agent_service/documents/arxiv/, kept apart from Aaron's drop folder so tb_list_documents still shows only hand-placed files. Citations from these are for ATTRIBUTION ONLY and never carry a proof step; see rule 12 of the v2 prompt.
• Coauthor invitations to the conversation partner are sent by the runner from inside the tool call that creates a draft (coauthors.py), however the draft was created, with an end-of-turn sweep as a backstop for one that did not land. The model is told not to send them itself. Timing matters here: a draft is visible only to its authors, so inviting at the end of a turn left a whole phase of drafts unreadable to the partner for as long as the turn ran, and lost them entirely if the process restarted mid-turn.
• The system prompt inlines the site's protocols.md, workflow.md and api-manual.md, fetched from the deployment (see "The content contract" below), plus collaboration rules (draft-first, invite only Aaron, never publish without approval).

Relationship to TheoremBase

This repository is not part of the site. It talks to a running deployment over the public HTTP API and knows nothing else about it: no database, no source tree, no shared code. Point AGENT_TB_BASE_URL at any deployment and these agents work against it.

That boundary is the point. The site defines what content must look like and how to get it published, and says so publicly; anyone can write an agent against those rules, in any language, and the site does not care how it works internally. What lives here is one such implementation - these particular agents, their prompts, their model choices, and the loop that drives them.

Consequently, anything that is a convention of this runner rather than of the site stays here: the /new, /clearboard, /high and /low chat commands, the subagent split, the model tiers. The site's API manual does not document them, and should not.

The content contract

The three normative docs are fetched from the deployment at startup (and again on every /new for the v2 coauthor, and hourly with the reviewer's full sweep), not vendored. Two more things are fetched at startup for the same reason: the kinds table (GET /api/v1/theorems/kinds, kinds.py) and the route table (GET /api/v1/openapi.json, routes.py), each with a fallback that keeps the runner working on an older deployment.

• GET /content — index of what is published
• GET /content/protocols.md — what content must look like
• GET /content/workflow.md — the draft, validate, publish loop
• GET /content/api-manual.md — endpoint reference

content_docs.py fetches them and inlines them into the system prompt, so an agent is always working from the rules the site is currently publishing rather than from a copy that drifted. Each fetch is mirrored to agent_service/state/<target>/content-cache/. If the site is unreachable the runner falls back to that cache and logs an error saying so; with neither source it refuses to start, because an agent with no contract authors against its own guesses, which is worse than being down.

Setup

python -m venv .venv
.venv\Scripts\Activate
pip install -r requirements-dev.txt
copy .env.agent.example .env.agent   # then fill in the account credentials

Also needed:

• A reachable TheoremBase deployment at AGENT_TB_BASE_URL (default http://127.0.0.1:8000).
• Claude Code CLI installed and logged in (the SDK uses its subscription credentials; no ANTHROPIC_API_KEY needed). A subscription login is for your own personal use only - see "Authentication and personal use". See also "Authentication expiry" below — OAuth credentials do expire, and a long-running runner will hit it.

Runtime versions are pinned in requirements.txt to the set the agents were already running under when they moved here; upgrading is a separate, deliberate step.

Configuration (.env.agent)

Agent settings live in .env.agent at the repo root (gitignored).

Variable	Default	Meaning
AGENT_TB_BASE_URL	http://127.0.0.1:8000	Backend base URL
AGENT_TB_EMAIL / AGENT_TB_PASSWORD	—	Agent's TheoremBase account
AGENT_CLI_PATH	auto-detected	Path to the Claude Code CLI executable
AGENT_MODEL	claude-opus-5	Model for the coauthor agent
AGENT_EFFORT	high	Reasoning effort
AGENT_OWNER	Aaron	The one account every agent serves, reviews for, and may message
AGENT_BLOCKED_PARTNERS	reviewer account	Usernames never responded to (loop guard)

AGENT_ALLOWED_PARTNERS, AGENT2_ALLOWED_PARTNERS and AGENT_REVIEWER_REPORT_TO are no longer used: if one names anyone other than AGENT_OWNER (including *), the runner refuses to start. | AGENT_POLL_SECONDS | 20 | Inbox poll interval |

Run

.venv\Scripts\Activate
python -m agent_service.runner

Then, from the frontend, log in as Aaron, open /messages, start a conversation with Claude-agent-v1, and send it a task. Typical flow:

1. You: "Let's work toward Stokes on manifolds. Start by finishing the boundary-of-a-manifold chain."
2. Agent: replies with a plan, creates/revises drafts, sends you coauthor invitations, and reports draft ids and validation results.
3. You: review drafts in the UI, accept invitations, reply with feedback.
4. Agent: revises until you say e.g. "publish the boundary trace theorem".
5. Agent: publishes that item only, quoting your approval.

V2 orchestrator agent (experimental)

.venv\Scripts\Activate
python -m agent_service.runner_v2

Account Claude-agent-v2 (AGENT2_* in .env.agent), same message loop as v1, but designed for phase-scale segments: one instruction can cover an entire dependency chain taken to publication-ready drafts. Differences from v1:

• Alignment first: it discusses the plan and pushes back on apparent misunderstandings until both sides agree, before starting large work.
• Subagents (SDK Task tool): tb-ops is a context shield - it absorbs verbose enumerations, corpus sweeps, and audits, returning compact digests so the orchestrator's context stays mathematical (dependent creates and judgment-laden validation stay inline), and it carries the batch tools (copy, batch substitution, refresh, tb_relate_many); draft-reviewer reviews every draft internally before the partner sees it - correctness, hypotheses, reference coverage both ways (nothing missing, nothing cited that the referenced material already licenses), definition discipline, and over-justification/readability, quoting the stored text verbatim in every finding. A fix that changes no mathematics is checked by validation and tb_diff_draft, not by a second review pass.
• Reviewer feedback is pre-triaged: the runner injects a digest of reviewer activity on the account's published items at the start of each session, fetched with max_comment_score=7, so a non-flag review comment scored 8 or higher is neither counted nor read; each line lists the scores of the comments that do count.
• Two model tiers (below), switchable per conversation from chat.
• Publishing still requires the partner's quoted approval - a phase ends at reviewed drafts, never at publication.
• State: sessions_v2.json / model_tiers_v2.json / system_prompt_v2.md in the target's state dir; logs in state/logs/coauthor_v2.log. v1 and v2 can run side by side (each blocks the other's account, so they cannot talk to each other).

Model tiers (v2)

The orchestrator and both subagents move together as a named set, defined by V2_MODEL_TIERS in config.py:

tier	orchestrator	draft-reviewer	tb-ops
high	Fable 5.1	Opus 5	Sonnet 5
low	Opus 5	Sonnet 5	Sonnet 5

high is what v2 has always run. low steps the two expensive roles down one model each; tb-ops stays on Sonnet in both, since its work is mechanical and the tier below would be a real drop in reliability. Dropping only the orchestrator would not be a cheaper configuration - on a phase-scale segment the reviewer subagent is a large share of the cost.

AGENT2_TIER picks the tier a fresh conversation starts on (default high); AGENT2_MODEL no longer applies to v2 and is ignored with a warning. Each partner's current tier is kept in model_tiers_v2.json, so a switch survives a runner restart and one conversation's tier never affects another's.

Reviewer agent

.venv\Scripts\Activate
python -m agent_service.reviewer

Every AGENT_REVIEWER_POLL_SECONDS (default 300) it lists all theorem cards and collects unseen latest_version_ids and published proof versions that its owner authored or coauthored (a statement when the owner is an author of the theorem, a proof when the owner is an author of the proof), grouped per theorem — a statement and its proofs are reviewed together in one SDK session because they share dependency context. Efficiency features:

• Runner-side preflight: before spawning a session, the runner checks the reviewer's own flags, verifies and comments (one version-card read per theorem version, two reads per proof version); already-reviewed items are skipped without any model cost (idempotent even if state is lost).
• tb_review_bundle tool: one call returns the statement, every proof body, and the full statements of all referenced dependencies, instead of the model fetching them one turn at a time. Dependencies come from the site's batch version card (POST /theorems/version/cards, 100 per call) rather than one read each, and the index marks open flags on a dependency and the clause anchors the reviewed text cites. When the items under review are themselves too long for one tool result, the largest body is clipped and the bundle names the exact tb_read_text call that reads the rest, instead of the whole result being lost.
• Redaction exposure: the bundle also calls redaction-exposure for each item under review and reports, in one section, any withdrawn item the content rests on — directly, or one step further down through a dependency that itself still stands. Depth 1 was already visible as a [REDACTED] mark in the dependency index; depth 2 was not visible at all, and the site's protocols bar a newly published version from depending on redacted items to that depth. A check that could not run says so rather than being omitted, since a missing section otherwise reads as "nothing found".
• Light/full sweeps: a light sweep reads only the catalog rows changed since the previous sweep (with an hour of overlap) and fetches proof lists only for theorems with a new latest version; every AGENT_REVIEWER_FULL_SWEEP_CYCLES-th cycle (default 12, i.e. hourly) reads the whole catalog and sweeps every theorem with proofs to catch proofs published later onto an old theorem version.
• Lean prompt: the reviewer system prompt carries the review policy, an endpoint cheat-sheet, and protocols.md only (~11K chars vs the coauthor's ~53K).

Review policy (see reviewer_prompts.py): verify only complete rigorous proofs and only well-typed, fully justified statements of the directly verified kinds (definition, axiom, setting, example, equation), flag statements and proofs with major defects, always post a structured comment (Evaluation / Assessment / Suggested changes / Decision) whose Evaluation number also travels as the comment's advisory score (enforced in the reviewer's tb_api: a non-flag review comment with an Evaluation line and no score gets it added before sending; flags and remarks carry none), thumbs at score >= 8 or <= 2, and a DM to its owner on every flag. It has no publish tool at all and is instructed never to author content. Which kinds take proofs and which are verified as statements comes from the site's kinds table (GET /api/v1/theorems/kinds, see kinds.py), fetched at startup and rendered into each task prompt, so a kind added server-side needs no code change here.

Besides the instant flag DMs, the runner sends the owner (AGENT_OWNER) a review digest DM — a linked list of everything reviewed since the last digest, with scores and verify/flag marks — at most once per AGENT_REVIEWER_REPORT_SECONDS (default 1800). The digest is composed by the runner from confirmed review outcomes (no model cost) and pending entries are persisted, so restarts neither drop nor duplicate them.

Reviewer settings in .env.agent: AGENT_REVIEWER_TB_EMAIL, AGENT_REVIEWER_TB_PASSWORD, AGENT_REVIEWER_MODEL (default claude-opus-5-5), AGENT_REVIEWER_EFFORT, AGENT_REVIEWER_POLL_SECONDS, AGENT_REVIEWER_FULL_SWEEP_CYCLES, AGENT_REVIEWER_BACKFILL, AGENT_REVIEWER_REPORT_SECONDS. On first run with AGENT_REVIEWER_BACKFILL=false (default) it baselines the existing corpus and only reviews content published afterwards; set it to true before the first run to review the whole backlog. To force a re-review of one item, remove its version id from agent_service/state/reviewer_state.json and delete the reviewer's prior comment (otherwise the preflight will skip it).

Sharing long source material (coauthor)

Drop files (e.g. a paper's LaTeX source) into agent_service/documents/ (gitignored) and tell the agent what to do with them. It discovers files via tb_list_documents and reads them in bounded line-range chunks via tb_read_document, so it works through long documents section by section instead of holding the whole file in context — and it can re-read from the file after a /new reset without you re-sending anything. The prompt requires derived content to be restated in site style with a citation to the source work, never pasted LaTeX.

Conversation whiteboard (coauthor)

Every conversation carries two persistent note panes — one owned by you, one by the agent — rendered beneath the message composer. They are the only memory that survives a /new reset, so the agent's pane is where the project roadmap, the settled design decisions, and the next step live.

Both panes are injected by the runner into the first turn of every session, before the partner's message, rather than left to the model to fetch. A reset session has no memory that the board exists, which is exactly when its contents matter most, so this is a runner guarantee and not a prompt rule. It happens only on a session's first turn — a resumed session already has the board in its history — and a whiteboard the runner cannot read is skipped rather than allowed to cost a turn. The injected sizes are logged. tb_read_whiteboard remains available for a mid-session re-read, e.g. after you edit your pane while the agent is working.

The half the runner cannot do is the writing. Routine updates go through tb_patch_whiteboard, which replaces, removes or appends ONE section of the agent's pane by its heading title (PATCH .../notes), leaves the rest byte for byte as it was, and cannot revert edits made since the agent last read the board; the pane's section titles are injected beside the board so a patch needs no re-read, and an unknown title comes back with the list for one retry. tb_write_whiteboard remains the full rewrite, for a phase turnover or after /clearboard.

Each author writes only their own pane, so the agent can never overwrite your notes and vice versa. Keep panes short — a plan, not a log of work done: the board is injected at the start of every session, so its length is a recurring cost, not a one-off. Bodies over 50,000 characters are rejected (the cap is read from every pane response and persisted per target; the constant in tools.py is only the fallback for a process that has not read a pane yet). The site keeps every version of a pane (GET .../notes/history, restorable from the page), so a rewrite or a /clearboard discards nothing for good.

Working notes (v2 coauthor)

The whiteboard is the plan you review. The agent also needs a memory that survives /new for what it would otherwise re-discover at a cost — which labels exist and what each defines, clause anchors and claim numbers, the setting stack, facts verified against stored text — and until 2026-09-18 that index was written onto the board too (40% of a 41k-char pane). It now lives in the agent's working notes: a private Markdown file per conversation under agent_service/state/targets/<site>/notes_v2/, never sent to the site and never shown to you, injected into the first turn of every session right after the board by the same runner guarantee.

The tools mirror the whiteboard's: tb_patch_notes replaces, removes or appends ONE section by heading title with the site's section semantics (a section runs to the next heading of the same or a higher level; titles match case-insensitively; fenced code is not a heading), tb_write_notes is the full rewrite, tb_read_notes the mid-session re-read. The pane is capped at NOTES_MAX_CHARS (30,000) in working_notes.py; the cost per session behind that number is in reports/agent-checkin-2026-09-18.md. Prompt rule 13 says which pane holds what. There is no chat command for the notes; read the file if you want to see them.

Chat commands (coauthor)

Commands go at the start of a message. The runner executes and strips them before the model sees the text, so they work regardless of how loaded the session is. A leading backslash works too (\new, for hands that have been typing LaTeX). They may be combined in any order (/new /clearboard <task>), and any of them may be followed by the instruction to act on; sent alone, the agent just confirms what it did.

• /new — reset that conversation's agent session (fresh context; an old session grows expensive to resume as history accumulates). Use it when switching topics. The v2 runner also re-fetches the content contract and rewrites the system prompt at that moment, so a site-side revision of the docs reaches the agent at the next /new rather than the next restart.
• /clearboard — empty the agent's own whiteboard pane. Use it when starting an unrelated project, usually together with /new. Your own pane is untouched; clear that yourself from the page. The runner's behaviour is unchanged by the whiteboard history: the cleared text is kept as a version server-side and can be restored from the page.
• /high, /low (v2 only) — move this conversation to that model tier. The switch takes effect on the same message and holds until changed. Giving both in one message changes nothing.

A tier switch does not reset the session: the CLI resumes an existing transcript under whichever model it is handed next, so models can change mid-phase without losing the work. What it does cost is the prompt cache, which is per-model — the first turn after a switch re-reads the whole session at full input price, which on a long session can outweigh a turn's saving. So pair the switch with /new when the conversation is moving on anyway (/low /new draft phase 3), and switch bare when the running context is the point. The v1 runner shares the command parser but has a single model, so it answers a tier command by saying it was ignored.

Logging

Both runners log to the terminal and to rotating files under agent_service/state/logs/ (coauthor.log, reviewer.log; 5 MB x 3 rotations, UTF-8), so runs are inspectable after the terminal is gone. What gets logged:

• every message received/replied, every tb_api/tb_publish call with method, path, and status (publish approvals at WARNING with the quote)
• agent> / reviewer> snippets of the model's intermediate commentary
• per-turn summaries: turns, wall seconds, cost, session id, and (v2) a tally of tool calls by tool and by tb_api path shape, so a long turn's log says what it was doing
• reviewer per-cycle lines (Cycle N (light|full sweep): K group(s) pending) and explicit Confirmed review posted for ... confirmations
• a coauthor heartbeat roughly every 5 minutes so silence is distinguishable from a hang; raw HTTP request noise (httpx) is demoted to WARNING

Reliability notes

• The reviewer marks an item reviewed only after confirming via the API that its review comment actually exists (a session that completed without posting leaves the item to retry). While any item has pending attempts, every cycle runs a full discovery sweep so retries happen within one poll interval.
• The coauthor re-delivers messages that were marked read but never answered (crash/restart mid-turn).
• Sessions blocked by expired credentials or an exhausted usage limit are detected before their output is used (see "Authentication expiry").

Authentication and personal use

The agents reach Claude through the Claude Code CLI, which authenticates in one of two ways:

• A Claude subscription (claude login). A subscription is for the subscriber's own, personal use. Run the agents on one only for yourself: as your own coauthor and reviewer, answering you and reviewing your work. Do not use a subscription to run agents that serve other people.
• An Anthropic API key (ANTHROPIC_API_KEY in .env.agent), under Anthropic's Commercial Terms. This is the route for anything offered to other users, and it would also need the owner-only restriction in config.py changed deliberately; it is not a configuration switch.

As shipped, every agent serves only AGENT_OWNER, which keeps subscription use personal.

Authentication expiry

The CLI returns Failed to authenticate. API Error: 401 OAuth access token has expired as the session's ordinary final text, in one turn, at zero cost. Nothing distinguishes it from a real answer except the content, so session_health.check_session inspects every session's text plus its cost and raises SessionBlocked when a zero-cost session reports only an auth or quota error. Without that check the coauthor sent the raw provider error to its partner as the reply, marked the partner's message answered, and lost it.

What each runner does when blocked:

• coauthor / v2 — no reply is sent and no session id is stored, so the partner's message stays unanswered and is re-delivered by the normal pending check once credentials work again. The runner logs an error and idles for BLOCKED_BACKOFF_SECONDS (5 minutes) instead of respawning a doomed session every poll.
• reviewer — the attempt counters incremented for that group are handed back and the cycle stops, so an outage cannot exhaust the retry budget and dead-letter the work.

Work is therefore held, not lost, and resumes on its own — but re-authenticating is a human step. To fix it:

claude login          # interactive; refreshes the stored OAuth credentials

Then restart the runners. For an unattended setup that does not expire, put a long-lived key in .env.agent instead:

ANTHROPIC_API_KEY=sk-ant-...

.env.agent is loaded into the process environment before any session starts, and the CLI subprocess inherits it.

State

• agent_service/state/sessions.json — coauthor SDK session id per partner (delete a key, or send /new, to give that conversation a fresh context).
• agent_service/state/reviewer_state.json — reviewed version ids + baseline.
• agent_service/state/logs/ — rotating log files for both runners.

The conversations themselves are not here. sessions.json holds only ids; the CLI keeps each transcript under ~/.claude/projects/<repo path with separators as dashes>/<id>.jsonl, so the session namespace is tied to this repository's path. Moving or renaming the repository orphans every stored id, and the CLI prunes transcripts after cleanupPeriodDays (30 by default). cli_sessions.py checks a transcript is reachable before resuming it and starts a fresh session with a note to the partner when it is not, rather than failing the turn.

State is per target: session ids and reviewed-version baselines only make sense against one deployment's database, so when AGENT_TB_BASE_URL points at a non-local host the runners keep their state under agent_service/state/targets/<host>/ instead. The local default keeps the flat layout above. Logs are shared across targets.

Running against a deployment (e.g. Fly)

The runners always execute on your machine (the SDK uses your Claude Code CLI subscription); only the API target changes. The deployed site proxies /api/v1/* through to the backend, so the public site URL works directly as the API base. In the terminal that launches a runner:

$env:AGENT_TB_BASE_URL = "https://www.theorembase.xyz"
python -m agent_service.reviewer

Requirements: the agent accounts must exist in the target database (restoring a local dump via scripts\db_restore.ps1 carries them over, same passwords), and the reviewer baselines the remote corpus on its first run unless AGENT_REVIEWER_BACKFILL=true.

Baseline gap: the first-run baseline marks everything currently published as seen — including anything published between seeding the target and the reviewer's first launch, which therefore never gets reviewed. To recover: stop the reviewer, remove the affected version ids from that target's reviewer_state.json (diff the target DB's theorem_versions / proof_versions ids against the seed dump to find them), and restart — the first cycle's full sweep picks them up.

Acknowledgements

Thank you to arXiv for use of its open access interoperability. The v2 coauthor agent searches arXiv through its public API and reads papers' HTML versions (see arxiv_client.py); it makes at most one request every three seconds and identifies itself in its User-Agent. Content taken from a paper is cited to it, and each paper remains under its own license.

License

Copyright (C) 2026 TheoremBase Contributors

This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License in LICENSE for more details.