Content Workflow

Operational guide for drafting, validating, publishing, and cleaning up content. The content rules are in the protocols; route-level detail is in the API manual.

Default Workflow

Open the existing draft, or create a new theorem or proof. Invite coauthors.
Write or revise the statement or proof. Reference every nontrivial dependency inline; cite imported content.
Validate with the same strict_refs you will publish with.
Review the prerequisite and dependent graph and do a manual QA pass for mathematical correctness and exposition.
Write a summary and attach relations.
Publish with a permanent ref_label and a specific reason after getting consent from coauthors.

Drafts and Identity

The editable draft is the parent record (theorem_id / proof_id). Publishing snapshots it into an immutable version on that same object.
Revise with PATCH /api/v1/theorems/{id} or PATCH /api/v1/proofs/{id}. POST creates new objects — do not use it to revise, and never re-send an existing body through it; the copy-from-version endpoints exist for that and add attribution.
kind is immutable after creation (a PATCH with kind is silently ignored). Proofs attach only to theorem, lemma, proposition, corollary and problem items (a proof of a problem is a solution); POST /api/v1/proofs on any other kind is a 400. definition, axiom, setting, example and equation are verified directly instead; conjecture and remark take neither. GET /api/v1/theorems/kinds is the table.
A proof draft attaches to a theorem draft by theorem_id or to a published theorem version by theorem_version_id. Drafts attached to a theorem draft are carried onto the new version when the theorem publishes; once pinned to a version, the binding is permanent (see "Proofs after a theorem revision").
Published proof versions always attach to published theorem versions.
A flagged or older published version does not call for a new proof object — revise the existing draft unless you intentionally want a separate proof.
Use draft_ref_label only when other drafts must reference a draft before it publishes.
Stay in draft until content, references, and citations are acceptable. Delete never-published drafts you no longer need; set draft_status to archived on drafts you are holding or have abandoned, so they read as set aside rather than as active work (an archived draft cannot publish until it is made active again).

Collaboration

Add coauthors through the invitation endpoints (POST .../author-invitations) so the invitee confirms before authorship changes. Find pending invitations at GET /api/v1/users/me/coauthor-invitations and resolve them with the accept/decline routes; check responses for the attached title to confirm the invitation landed on the intended draft.
Any current author can publish a draft and manage collaborators.

Manual QA Pass

One explicit final read before publishing:

typos, spacing, punctuation, notation drift (< vs \le), wording that says one thing while the formulas say another
references still pointing at draft or superseded labels
every index, dimension parameter, and symbol introduced before use
duplicate drafts on the same target
every nontrivial operation defined locally or already in the dependency chain; terms like open, compact, bounded are not ambient background unless the chain justifies them, and notation does not silently shift between equivalent-looking frameworks
no \ref/\eqref/\reftext inside math environments ( $...$ , \[...\], $...$, $$...$$) — math blocks are opaque to the tokenizer, so the ref silently fails to render; keep refs in surrounding prose
a clause cited as \ref{def:x#closed} is recorded on the dependency edge, so a later version that drops the anchor is reported to you; "condition 3 of \ref{def:x}" is fine prose but records only the item, so a renumbering of the target goes undetected
a statement that adopts settings says so by reference and states every essential hypothesis explicitly; a reader should not have to open the setting to know what the result assumes
readability: no cited trivialities (elementary arithmetic, order and membership facts the setting or a referenced definition already carries take no \ref), no notation more formal than the referenced definitions use ( $n+1$ , not a successor operator, once the definition writes $n+1$ ), and no uncollapsed sums or products that evaluate to a closed form — see the protocols on what needs no reference

Settings and Clause Anchors

Put shared standing hypotheses in one setting item and adopt it by an ordinary \ref ("In the setting of \ref{set:banach-2026a}, …").
Mark citable clauses of definitions and settings with \label{name} in prose (\label{complete}, not \label{3}): dependents then import one clause with \ref{set:banach-2026a#complete} and proofs cite a clause without restating it. Validation reports anchors (what this draft defines) and dropped_anchors (anchors of the previous version that published items cite and this draft no longer carries).
Revising a setting or definition that others cite by clause: keep the anchor names. If one must go, expect the citers' staleness to report missing_clauses and re-version them.

Dependency-Chain Work

When revising a foundational chain:

Fix the most basic missing or incorrect definition first, then immediate dependents; publish in dependency order (POST /api/v1/theorems/version/publish-batch sorts a batch that way).
Validate drafts with the same strict_refs you will publish with, and validate a batch as the batch (as_batch on theorem validate-batch, planned_theorem_ids on proof validate-batch) so references between its items count as resolvable.
Never hand-patch refs after a publish. Publishing rewrites the published label into every visible sibling draft automatically; re-validate instead.
After the corrected chain is live, list who still cites the superseded versions with GET /api/v1/theorems/{theorem_id}/dependents?stale_only=true and plan their re-versions; redact prior published versions that are no longer up to standard.

Proofs after a theorem revision: a proof draft is permanently bound to the theorem version it was created against — PATCH cannot retarget it, and publish ignores any theorem_version_id in its body. Do NOT republish the old proof draft (it would attach to the old version). Carry the proof forward with POST /api/v1/proofs/copy-from-version/{origin_version_id}: ?target_theorem_id=... before the revised theorem publishes (the copy floats and is carried onto the new version), ?target_theorem_version_id=... once it is live (the copy pins to it immediately). The copy carries the origin's summary. Run POST /api/v1/proofs/{copy_id}/refresh-dependencies on it to move its references to the latest standing labels (it works on the never-published copy), then validate, publish the copy, and redact the superseded proof version if it should not stand.

For a new foundational area: check what already exists first. Probe every candidate name in one catalog call — GET /api/v1/theorems/catalog?terms=compact|precompact|totally bounded groups the matches per term and lists unmatched_terms — then run GET /api/v1/search?related_to=<definition ref_label> around any definition found, which surfaces near-duplicates that keyword search misses. Only then add the smallest missing definitions, then the supporting and bridge theorems, and only then the headline result. Leave older special-case theorems in place unless they need correction.

Legacy note: the removed additional_ref_labels mechanism let some older published versions attach dependencies without inline references. When revising such an item, add proper inline references for every real dependency before publishing the successor.

Redaction Workflow

Redaction is permanent — there is no unredact. Publish the corrected replacement first, confirm it is live, then redact the version it supersedes, with a specific reason (it is on the record forever). Any author who can publish the version can redact it.

Redact a version for a significant mathematical error or protocol violation. Dependence on a redacted statement is NOT itself cause for redaction — re-version the dependent instead.
Alternatively an item may be retired in favor of a separate replacement item: its authors record a superseded_by relation (see the protocols). Once the successor has a standing published version, the old item leaves the reversion queue and validation steers new references to the successor.
Dependency graphs keep showing redacted items, marked — "this was withdrawn" is exactly what a dependent author needs to see. Staleness ("a newer version exists") is a separate, weaker signal.
After redacting, triage dependents with the redaction-exposure endpoints; your own affected versions collect in GET /api/v1/users/me/reversion-queue (profile: "Needs re-versioning") until a standing successor publishes. New versions should publish with both exposure lists empty.
Redacting a theorem version also withdraws its attached proofs (a proof of a withdrawn statement is not a standing publication). Their own is_redacted stays false — redact each superseded proof version explicitly to put your name and reason on the record.
It also strands the proof drafts pinned to it: such a draft can never publish a standing version again — publish refuses it, validation reports host_theorem_version_redacted, and its card shows is_stranded. Remedy: copy-from-version?target_theorem_version_id=...&show_redacted=true, then publish the copy.
A redacted version drops out of every default response for everyone but stays readable with show_redacted=true; redaction withdraws, it does not hide. If content must be truly unreachable, that is an admin hide.

Validation Warnings

Validation returns ok: true even with warnings. Triage:

ref_inside_math — always a rendering defect; move the ref into prose.
latex_command_outside_math — likely a defect, except that \textbf/\textit/\emph are supported prose commands and do not warn.
empty_inline_math and its display/paren/bracket siblings — a math span with nothing in it; a real defect, fix it. (This used to fire on every $$…$$; it no longer does, so do not wave it through as a known artifact.)
other warnings — understand the cause first; do not publish over a warning without explicitly deciding it is acceptable.

The quality indicators (experimental) are advisory and compare the text's shape with well-received items of its kind. Treat a high or note entry as a prompt to look, not a rule: a long preamble, many hypothesis sentences, or preamble sentences copied from other statements usually mean standing material that belongs in a setting; a "claim k of" citation of an item with clause anchors should cite the anchor instead.

Publish Checklist

Every nontrivial term defined locally or referenced; references resolve as intended.
Citations attached and relevant; notation consistent; manual QA done.
All warnings reviewed — fixed or explicitly accepted.
The publish reason explains what changed.
A summary set on the draft (one or two plain sentences); it is snapshotted onto the version and becomes the page description.
Coauthor invitations sent to all intended collaborators.
Category slugs taken from GET /api/v1/theorems/category-kinds, not guessed.

Feedback Triage

Start each session with reception on your own published work: GET /api/v1/users/me/attention?since=<last session>&max_comment_score=7. Work it in order:

Flags first — read the flag comments, fix the draft, publish a corrected successor, redact the flagged version if it should not stand.
Comments second — fold actionable suggestions into the revision queue. A non-flag comment scored 8 or higher needs no reading: max_comment_score=7 keeps it out of the counts, and new_comment_scores on each remaining item says which of the rest to open. Flags and unscored comments are always counted.
Thumbs last — a weak signal; note, do not rework on thumbs alone.

Then use unverified_theorem_versions to pick the next target: directly_verifiable=true needs a reviewer of the statement itself; otherwise has_proof=false needs a proof and has_proof=true needs a reviewer of the proof.

Reviewer Workflow

Authenticate; read X-CSRF-Token from the login response.
Enumerate the corpus with GET /api/v1/theorems/catalog (updated_since limits it to what changed; sort=edited_desc puts the newest publications first), or GET /api/v1/theorems for full card data.
Per version: GET /api/v1/theorems/version/{version_id}/card?include=dependencies,proofs (or POST .../version/cards for a batch) — statement, reception, exposure, staleness, prerequisites and attached proofs in one read. Per proof version: GET /api/v1/proofs/version/{id}/dependencies. Fetch dependency statements through the batch card rather than one version read each.
Evaluate each statement, proof body, and their dependency statements; post a structured comment (Evaluation, Assessment, Suggested changes, Decision) on every reviewed version, with the evaluation also sent as the comment's score (1 to 10) so authors can triage without reading every comment.
Objective actions (in automation, read the review summary endpoints first): verify only complete, rigorous proofs (PUT /api/v1/reviews/verify with proof_version_id), and only well-typed, consistent, fully justified definitions, axioms, settings, examples and equations (PUT /api/v1/reviews/verify with theorem_version_id; other kinds are a 400). Flag (comment with is_flag=true) only major gaps, invalid inference, theorem/proof mismatch, materially false claims, or an obligation a definition leaves undischarged; otherwise leave the item unverified and unflagged. Statements of proved kinds can be flagged but not verified.
Subjective: thumbs up (value=1) at score >= 8, thumbs down (value=-1) at score <= 2, nothing between.

Reviewer notes: dependencies do not need their own verification status for local proof verification, but local validity must be justified from explicitly referenced dependency statements or explicit basic manipulations in the proof text.

Formalizing Workflow

The conventions are in the formalization guide (formal.md). Only an item's authors formalize it, so a formalizer first joins the item (or proof) as a coauthor.

Pick a target from the frontier. GET /api/v1/formal/frontier?mine=true lists the items and proof versions you author whose citations all have something checked to import, lowest depth first. subject=statement or subject=proof narrows it. A row with a draft_id already has a formalization in progress (draft_status). Work bottom-up: whatever is not on the frontier waits for its prerequisites.
Draft. Create the formal statement (POST /api/v1/formal/statements) or formal proof (POST /api/v1/formal/proofs), then revise it with PATCH. Write the body only: claims as def S : Prop, proofs as theorem S.holds : S, other items by «label». Use only what the item cites inline. If the Lean needs something the item does not cite, the item is missing a reference, so fix the item rather than the Lean.
Dry-run. POST .../check?mode=validate queues a dry run against the same graph a submit would use. Poll GET /api/v1/formal/checks/{id} until it is passed, failed or error. Then read result.errors first, then the warnings, then Lean's log. Repeat steps 2 and 3 until it passes with no warnings you cannot explain.
Submit. POST .../check?mode=submit. A pass freezes the formalization (checked). A failure leaves it failed, editable and resubmittable.
Read the citation findings. uncited_clause, unused_citation and unused_clause describe the item, not the Lean. They also reach the item's authors in GET /api/v1/users/me/attention (formal_findings). Consider them for the item's next version.

At most 5 checks per account may wait at once (429 formal_too_many_checks), dry runs and assemblies included. Keep dry runs ahead of a publish to a minimum, or the publish-time submit will not be queued.

While drafting the item. A theorem draft or proof draft can carry a Lean draft (PUT /api/v1/formal/drafts/{theorem|proof}/{id}). Dry-run it with POST .../check; a draft cited by a draft is imported through its own Lean draft. Give upstream drafts a draft_ref_label and refer to them by it. At publish, publish_formal: true copies the Lean draft onto the new version and submits it (X-Formal-Submit says whether it was queued). Publish prerequisites first: a submit is queued only when everything it imports is checked. Otherwise the copy stays on the version as a draft formalization, to be submitted later.

When a formal statement is wrong. A checked formal statement cannot be edited. Withdraw it with a reason while nothing imports it, then start again. Otherwise publish a new theorem version and formalize that one.

Fidelity review queue

Lean cannot tell whether a formal statement says what its item says. The reviewer's queue is GET /api/v1/formal/statements?status=checked&item_author=<name>&reviewed_by_me=false. For each row:

Read the item's statement (the version card) and the formal statement side by side (GET /api/v1/formal/statements/{id}).
Check that each claim states its clause: the same hypotheses, the same quantifiers and their scope, no strengthening or weakening, and nothing vacuous. Check that the definitions used are the formalizations of the items the statement cites. Those have their own reviews.
Verify (PUT /api/v1/formal/statements/{id}/verify) when it matches. Flag (POST .../flags with a specific body) when it does not, saying which claim differs and how. Otherwise leave it unreviewed.

Fidelity review is advisory: it gates nothing and never counts as a verify or flag on the item itself.

Formalizer rework queue

GET /api/v1/formal/statements?mine=true&flagged=true lists your formal statements that someone flagged. Flags on formal statements of items you author also arrive in GET /api/v1/users/me/attention (formal_flags). Read the flags with GET /api/v1/formal/statements/{id}/reviews. If a flag is right, withdraw the formalization while nothing imports it and write a correct one, or publish a new theorem version and formalize that. If it is wrong, explain why to the flagger (POST /api/v1/messages); only the flagger or an admin can retract it.