DDocs∋Writing & formatting

The markup

Article fields are plain text with a few pieces of markup:

$…$

Inline math (Typst syntax), sits in a line of prose.

$$…$$

Display math: a centered block that can scroll on narrow screens. Prefer this for long formulas.

[[slug]]

Cite another article by its slug. [[slug|label]] sets the visible text. Citations in a statement or proof build the dependency graph; see Conventions.

**bold**

Bold text for emphasis.

hl("key", …)

Highlight a piece of notation, paired with @key{…} around the matching words in the in words reading. Same key, same color; see Statement and in words below.

The gloss and in words fields are plain English, not math: keep them free of $…$. And no em dashes anywhere; use a comma, colon, or parentheses instead.

Math is Typst

Math is written in Typst, which reads like the words you would say out loud, with no backslashes. Everything you submit is compiled server-side; anything that does not compile is rejected, and the editor previews it live as you type. A quick tour:

forall x, exists y

Quantifiers: for all x, there exists y.

x in A, x in.not A

Membership and its negation.

A subset.eq B

Subset-or-equal. Also union, inter, without (set minus), emptyset.

P and Q, P or Q, not P

Logical connectives.

P -> Q, P <=> Q

Implies, and if-and-only-if.

x_1, x^2

Subscripts and superscripts.

{ a, b }

Literal braces make a set.

cal(P)(A)

Calligraphic letters, e.g. the power set of A. Also cal(F).

For the full language, see the Typst math reference and the symbol index.

House notation

To keep 100+ articles consistent, some notation is defined once, site-wide, and available in every formula. Use these instead of rolling your own:

pair(a, b)

An ordered pair or tuple, rendered in angle brackets: ⟨a, b⟩. Nestable, e.g. pair(a, pair(b, c)). Use it for every ordered-pair object (memberships, set-builders, structures like pair(G, star)). Keep round parentheses for function application and grouping.

emptyset

The empty set, as the round ⌀ glyph.

S(x)

The successor of x.

A slash R

A quotient, e.g. a set modulo an equivalence. Always write slash; a literal / renders as a fraction.

A without B

Set difference (set minus).

a divides b

Divisibility. Also approx for approximately-equal.

g star h

A generic group operation.

f harpoon.tr A

The restriction of a function f to a set A.

abs(x), cases(…)

Absolute value, and a brace for case splits. exists! for unique existence.

Long formulas clip on phones when inline. Put anything wide in $$…$$ display math, which scrolls in place.

Statement and “in words”

Every article carries a formal statement (the notation) and an in words reading: the same statement said aloud in plain English. Both are required. The article page renders the formal statement in a box with the plain-English reading on a card below it, so write the prose as one self-contained sentence a reader could follow without parsing the symbols.

You can color-link the two, so a reader learning the notation sees which symbols a phrase stands for. Wrap a piece of the notation with hl("key", …) and the matching words with @key{…} sharing the same key. Each key gets its own color, and the “in words” card grows a toggle that lights up every matched pair on both sides at once. Keys are yours to name (e.g. all, divisor); the toggle only appears when an article uses them, and highlights are off until a reader turns them on.

$$hl("all", forall x) space not (hl("mem", x in x))$$

@all{Every set x} is not @mem{a member of itself}.

Only the statement and in-words fields are linked this way. Write @key{…} only where you want a highlight; it is markup in every prose field, so avoid it in ordinary text.

Mathlib links

When an article has a formal counterpart in Lean 4 / Mathlib, give its declaration name (e.g. Nat.add_comm) and a direct link to the docs. The article page renders it as a clickable link straight to the formal proof. Use the canonical share URL:

https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Nat.add_comm#doc