TheoremBase Protocols

This page is the normative content contract for TheoremBase. These protocols apply to every item and proof added through the UI or API.

Content Standards

Correctness and completeness are the author's responsibility.
Statements must be precise and use explicit assumptions.
Every nontrivial term used in a statement or proof must be defined locally or referenced explicitly.
Every symbolic parameter appearing in a statement or proof should be introduced explicitly.
Keep math and prose notation consistent.
An item or proof may carry a summary: one or two plain sentences saying what it says or how it proceeds, for readers scanning a list. A summary describes; it makes no claim beyond the statement and is not part of the logical record.
A later, more general theorem does not by itself make an earlier special-case theorem obsolete. Duplicates, competing approaches and differing levels of formality are expected.

Item Kinds

Proved kinds — theorem, lemma, proposition, corollary, problem. Their statements are established by proof objects attached to them. A proof of a problem is a solution: the same object, displayed under that name.
Verified kinds — definition, axiom, setting, example, equation. They take no proof. A reviewer verifies the item as stated: it is well-typed, internally consistent, and every claim it makes is justified inline or by reference. Well-typed means every symbol and operation is used as the referenced definitions permit: each object is introduced before use and nothing is applied outside what its definition allows. Verification is the reviewer's judgement and is not gated by validation.
Discussed kinds — conjecture, remark. They take neither proofs nor verification; comments, flags and thumbs only. A conjecture that acquires a proof should be published as a new theorem item, with the conjecture retired by superseded_by.

References, Labels, and Formatting

Every term whose meaning is fixed by a TheoremBase item, and every result an item relies on, must be referenced inline with \ref{...}, \eqref{...}, or \reftext{...}{...}. A term with no such item must be defined locally. There is no separate "ambient" dependency list; if something is in the dependency chain it must appear in the statement or proof body.
A reference records a dependency. A referenced setting carries its hypotheses, notation, and background results into the dependent, which may use them and their elementary consequences without citing each one.
A proof step requires a reference when its justification lies outside the item and the material it already references. A step whose justification is a result the item does not reference is a gap, however short the step reads.
\ref{}, \eqref{}, and \reftext{}{} are processed before the math renderer and must appear in prose only. They do not work inside any math environment ( $...$ , \[...\], $...$, $$...$$). To link a symbol that appears in math, introduce the reference in surrounding prose (e.g., "…for every \reftext{def:natural-numbers-2026a}{natural number} $m$ …"), then use the plain symbol in the math expression.
A statement may mark a clause with \label{name} in prose (never inside math), and other items may cite that clause as \ref{ref-label#name} or \reftext{ref-label#name}{text}.
\textbf{...}, \textit{...}, and \emph{...} are supported prose-formatting commands rendered as bold or italic. Use them freely in prose. \reftext{}{} and inline math ( $...$ ) may appear inside them. Do not use \textbf or \textit inside math environments; use \mathbf or \mathit there instead.
Use ref_label only for published, stable references.
You may use draft_ref_label on theorem drafts when other drafts need to reference them before publish.
Each ref_label is globally unique across all published versions of all theorems. A corrected or updated version must use a new label, typically by incrementing the letter suffix (e.g., 2026a → 2026b).

Definitions

A definition item states the definition only and any motivation or consequences belong in separate remark, lemma, proposition, or theorem items.
One concept per definition item, unless the parts are inseparable: a structure together with the operations it is defined with is one concept.
Any assertion in a definition must be stated so that its obligations are either justified from the stated assumptions or discharged through an inline reference. It must not leave the obligation to the reader or to the theorems that use it.
Verification of a definition means: well-typed, every obligation of assertions discharged as above, no claim beyond the definitional ones.

Settings

A setting is a named bundle of standing hypotheses, notation, and background results. It does not introduce new concepts, and it carries background results by reference rather than restating them.
A statement adopts a setting by an ordinary inline reference, and may adopt several. A setting carries the broadly contextual assumptions a body of work shares. Any hypothesis a particular result actually turns on is stated in that result, not left to a reference. A reader should learn what a result assumes from the result itself.
A setting asserts nothing new and is verified like a definition: well-typed, consistent, and notation introduced before use. Use clause anchors inside settings so dependents can import one hypothesis (\ref{set:x#complete}) rather than all of them.

Examples, Equations, Axioms, Conjectures, Remarks

An example is an expository item that exhibits an object satisfying (or failing) a definition or hypothesis. It must justify every claim it makes, inline or by reference to a published result; that justification is what a verifier checks.
An equation names a displayed equation, inequality or system for reference by other items. It asserts nothing about solutions; existence and properties belong in results that cite it.
An axiom is verified as well-typed and internally consistent as stated.
A conjecture states a precise claim believed but not proved. A remark records an observation or caveat that is not itself a result. Neither is verified; both may be commented on and flagged.

Relations

Relations are a curated, mutable map of how items relate as ideas. They are navigation aids, never part of the logical record, and never a substitute for an inline \ref{...} dependency.
concerns points at the definition item for a concept, which is how a result is marked as being about it. Definition items are therefore the concept vocabulary; settings are not concepts and cannot be concerns targets.
generalizes runs from the general item to the special case. equivalent_to, analogous_to, converse_of, and see_also are symmetric — record them once, in either direction.
superseded_by runs from a retired item to the separate item that replaces it. Unlike other kinds it is an authorial act, not open curation: only the superseded item's authors may record it.
Prefer the most specific accurate kind; use see_also only when none fits. Add relations sparingly, and never where an inline reference already says the same thing.
Relations attach to items, not to versions or proofs, and survive republishing.
Any account may add a relation; its creator, either item's authors, and admins may remove one. Removal is not a moderation action.

Attribution

Any content drawn from an external source must have a citation.
Copied or adapted content — external or internal — must be cited explicitly; for internal TheoremBase content the citation or attribution note must make the source version explicit.
If content is copied from an existing TheoremBase theorem or proof version into a new draft, preserve or refine the suggested attribution before publish.
Citation notes should distinguish adaptation from verbatim copying when relevant.
Do not represent copied material as original work.

Collaboration

For an existing theorem or proof, revise the existing draft object unless you are intentionally creating a separate replacement or branch.
A theorem or proof object has one collaborator set at the parent-object level, and published versions inherit that authorship display.
Any author on a draft may publish it and manage collaborators. That is the permission, not the norm: publish with the consent of the other authors, since a published version carries all of their names.
The primary author remains the canonical first author unless authorship is revised explicitly.
Collaborator additions should use invitation and acceptance flows so coauthorship is confirmed by the invitee before authorship changes.

Publishing

Drafts are for work in progress. Publish only when the content is acceptable as a public version, is mathematically correct, and meets TheoremBase protocols.
Validation is advisory. It helps detect structural problems but does not replace mathematical review or exposition review.
Strict publish should be used when you expect all references to resolve to published labels.
Draft-only references are acceptable in draft workflows but should not remain for strict publish.
Do not build on flagged content: validation reports referenced versions that carry an open flag (flagged_dependencies); read the flag before relying on the reference.
Publish with a clear, specific reason.

Redaction and Supersession

A theorem or proof version is redacted only for a significant mathematical error or a violation of TheoremBase protocols. Redaction is permanent and cannot be undone.
Being superseded by a newer version is not a reason to redact: staleness is reported separately and the older version keeps standing. Redact the older version only if it is itself wrong.
If possible, a corrected version should be published before the superseded public version is redacted. Redacting every published version of an item is also acceptable when new content replaces it.
Theorem or proof versions that depend on a redacted statement should be re-versioned, but dependence on a redacted statement is not in itself cause for redaction. Re-versioning leaves the superseded version stale; new references should target the newest standing version.
Instead of re-versioning, an item may be retired in favor of a separate replacement item: its authors record a superseded_by relation pointing at the new item.
Newly published versions should not depend on redacted items to a depth of 2: no direct dependency may be redacted, and no direct dependency may itself directly depend on a redacted version. When this is an obstacle it is preferable to re-version dependencies or create new content than to work around it.

Review

verify on a proof version means: a complete, rigorous proof of the statement it is attached to.
verify on a theorem version is available only for the verified kinds (definition, axiom, setting, example, equation) and means: well-typed and internally consistent as stated, with every claim justified inline or by reference. It is the reviewer's judgement; validation does not gate it.
Use flag comments on theorem versions or proof versions for major logical gaps, incorrect inferences, theorem/proof mismatch, materially incorrect claims, or an obligation a definition leaves undischarged.
Statements of proved kinds may be flagged and commented on but are not subject to verify; their verification lives on their proofs.
A review comment may carry an advisory score (1 to 10): the reviewer's overall impression, for the author's triage. It never gates verify or flag — a low score is not a flag, and a high score is not a verification.

Lean Formalization

A published version may carry a Lean formalization, under the conventions in the formalization guide (formal.md). Formalization is optional. The item's text is the mathematics, and a formalization never changes what the item says.
Only an item's authors formalize it: its formal statement is written by the item's authors, and a formal proof by the proof's authors. Someone else who wants to formalize an item joins it as a coauthor through the invitation flow.
One formalization per version: at most one standing formal statement per theorem version, and one formal proof per proof version. A formalization that passes its submit check is frozen.
Formalization goes bottom-up: a formalization imports only checked formalizations of the items its version cites.
"Matches the statement" (fidelity) review is advisory: verifying or flagging a formal statement gates nothing, and a fidelity flag is not a flag on the mathematics.
The fix for a formal statement that does not say what its item says is a new theorem version with a new formalization, or withdrawal of the formalization while nothing uses it (withdrawal is refused while checked work imports it). A checked formalization is never edited in place.

API Rules

Use API endpoints for theorem, proof, citation, collaboration, and moderation workflows. The user interface goes through the same API endpoints.
Do not read or write theorem, proof, citation, comment, feedback, or review content directly in the database.
Use Alembic migrations only for schema and static bootstrap data.