aris-pub/rsm/docs

RSM — Readable Science Markup

RSM is a web-first markup language for scientific manuscripts. It uses colon-delimited tags (:tag:) and Halmos closers (::) to express document structure, mathematical proofs, cross-references, and metadata.

Every .rsm file is a valid RSM manuscript.

Two Tag Types

RSM has two kinds of tags:

Block tags — structural containers (theorems, proofs, sections, lists, etc.)

:theorem: {
  :title: Main Result
  :label: thm-main
}
 
  Content paragraphs, nested blocks, inlines...
 
::

Inline tags — annotations within a paragraph (spans, refs, math, proof constructs)

:let: $x \in A$ ::
:claim:{:label: my-claim} some statement ::
:span:{:strong:, :emphas:} important text ::
:ref:label, display text::

Both open with :tagname: and close with :: (the Halmos). Sections are the sole exception — they close implicitly when a sibling or parent section begins, or at document end.

Document Structure

A manuscript starts with an optional title line using #, followed by optional top-level meta, then body content:

# Manuscript Title {
  :label: my-manuscript
}
 
:config: {
  :theme: default
  :accent: blue
  :typography: sans-serif
  :numbering: section
  :override-date: 2025-01-15
}
::
 
:author: {
  :name: Jane Doe
  :email: jane@example.edu
  :affiliation: Some University
} ::
 
:abstract:
  Summary of the manuscript.
::
 
:toc:
 
## First Section
  Content...
 
### Subsection
  Content...
 
#### Subsubsection
  Content...

Manuscript meta goes in {...} right after the # title. It accepts keys like :label: and :title:.

`:config:` is a block tag for document-wide settings: :theme:, :accent:, :typography:, :numbering:, :override-date:, :toc-depth:, :author-display-first:, :author-display-last:. It appears as a top-level block, closed with ::.

Section shortcuts: ##, ###, #### work like Markdown headings. They can also be written as :section:, :subsection:, :subsubsection: with a {:title: ...} meta key. Section-form tags do not need a Halmos — they close implicitly.

Sections can carry meta on the line after the heading:

## My Section {
  :label: sec-intro
  :icon: star
}

:appendix: is a stamp (no content, no Halmos) that marks where appendix sections begin.

Complete Tag Reference

Block Tags

All block tags open with :tag:, take optional {meta}, contain paragraphs/blocks, and close with ::.

Inline Tags — General

:span: is particularly useful for labeling a piece of text so it can be cross-referenced. The reference targets only the span, not the enclosing paragraph:

Some :span:{:label: key-insight} remarkable observation:: that we revisit later.
...
As noted in :ref:key-insight::, ...

Inline Tags — Special Syntax

Stamps (:prev:, :prev2:, :prev3:) have no content and no Halmos — they stand alone.

Emphasis shortcuts: **bold** = :span:{:strong:}bold::, *italic* = :span:{:emphas:}italic::.

Inline Tags — Proof Constructs

These appear inside theorem statements and proof steps:

All constructs except :qed: open with :tag:, take optional {meta}, contain inline content, and close with ::. :qed: is a stamp.

Meta Regions

Meta appears in {...} immediately after a tag. Block meta uses newline-separated key-value pairs; inline meta uses comma-separated pairs inside {...}.

Block meta (one pair per line):

:theorem: {
  :title: Main Result
  :label: thm-main
  :icon: star
}

Inline meta (comma-separated, on one line):

:span:{:strong:, :emphas:} text ::
:claim:{:label: my-claim} statement ::
:paragraph:{:icon: bookmark} Text here.

Meta Keys by Type

Text keys (value is a string on the same line or rest of line):

Boolean keys (presence = true, no value needed):

List keys (value in {item1, item2, ...} or a single item):

Any-value keys (parsed as-is):

Proof Architecture

RSM's structured proof system is inspired by Leslie Lamport's "How to Write a 21st Century Proof" and resembles the hierarchical proof style used in TLA+. Unlike TLA+ (which targets formal verification), RSM proofs are written in natural language for human readers — the structure provides navigability and rigor without requiring machine-checkable logic.

Proofs follow a rigid nesting: proof → steps → substeps/subproofs.

:proof:
 
  :step: {:label: step-1}
    Statement of what this step establishes.
 
    :p: Justification for this step. :: ::
 
  :step:
    :claim: Some intermediate result. ::
 
    :p:
 
      :step: Substep inside the justification. ::
 
      :step: Another substep. ::
 
    :: ::
 
  :step: :qed:
 
    :p: By :ref:step-1::. :: ::
 
::

Key rules:

• :step: can only appear directly inside :proof:, :sketch:, or inside a :p: (subproof)
• :p: provides the justification for its parent step — it can contain nested steps
• :p: closes with :: :: (its own Halmos, then the step's Halmos)
• Proof constructs (:let:, :assume:, :prove:, :claim:, :pick: / :st:, :qed:) appear inline within steps
• :qed: is a stamp — it has no content and no Halmos

Proof vs Sketch

:proof: contains the full structured proof with steps. :sketch: is a lighter variant — it has the same nesting rules but is intended for informal proof outlines. A common pattern is to place a :sketch: before the :proof: to give the reader a high-level overview:

:theorem: {:label: thm-main}
  :claim: All $X$ are $Y$. ::
::
 
:sketch:
  The idea is to use induction on $n$, applying Lemma 2 at each step.
::
 
:proof:
  :step: ...
  ...
::

Referencing Previous Steps

Inside a proof, you can reference earlier steps without explicit labels using stamps:

These are stamps — they stand alone with no content and no Halmos:

:step: {:label: stp-main}
  :claim: $a_n^{m+1} b_0 = 0$ ::
 
  :p: By :ref:first-substep::. :: ::
 
:step:
  :claim: $1 + u^{-1}x$ is a unit. ::
 
  :p: By :prev:. :: ::
 
:step:
  Multiplying :prev2: by $\lambda$ and subtracting :prev:.
::

For steps further back or across subproofs, use explicit :label: / :ref: pairs instead. :previous: is the non-stamp variant that takes a step number: :previous:3, Step 3::.

Common Proof Construct Patterns

% Introduce a variable
:let: $x \in A$ ::
 
% Introduce a variable with a property
:pick: $n \in \mathbb{N}$ :: :st: $x^n = 0$ ::
 
% Set the goal
:prove: that $1 + x$ is a unit ::
 
% State a claim
:claim: $f$ is nilpotent ::
 
% Alternative claim syntax
:⊢: $u^{-1} x$ is nilpotent.::
 
% Change the goal
:suffices: to show that $g$ is a unit ::
 
% Introduce an assumption
:assume: $f$ is a unit in $A[x]$ ::
 
% Introduce notation
:write: $A[x]$ for the ring of polynomials ::
 
% Mark goal as proven
:qed:

Extended Proof Example

A multi-level proof showing nested subproofs and step references:

:proof:
 
  :step: {:label: x-is-nilp}
 
    :pick: $n \in \mathbb{N}$ :: :st: $x^n = 0$ ::.
 
    :p: Such an $n$ exists by definition of nilpotent. :: ::
 
  :step:
 
    We have
    $$ {:label: eqn-main}
    (1 + x)(1 - x + x^2 - \ldots + (-1)^n x^n) = 1.
    $$
 
    :p: Multiplying the left-hand side directly yields the middle expression.
    The term $(-1)^n x^{n+1}$ equals $0$, by :ref:x-is-nilp::. :: ::
 
  :step: :ref:goal-1, Goal 1:: is :qed:.
 
    :p: By :ref:eqn-main::. :: ::
 
  :step: {:label: sufficiency}
 
    To prove :ref:goal-2, Goal 2::, it :suffices: to :assume: $u \in A$ ::
    where $u$ is a unit ::, and :prove: that $u + x$ is a unit. :: ::
 
  :step: :⊢: $u^{-1} x$ is nilpotent.::
 
    :p: Immediately from $(u^{-1} x)^n = u^{-n} x^n = 0$. :: ::
 
  :step: :⊢: $1 + u^{-1} x$ is a unit.::
 
    :p: By :ref:goal-1, Goal 1::. :: ::