Mathematical writing

In June 1993 Andrew Wiles announced a proof of Fermat's Last Theorem. The manuscript, some two hundred pages long, went to referees, who read it line by line. In September one of them, Nick Katz, asked a question about one step that Wiles could not answer: there was a gap. A year later Wiles, working with his former student Richard Taylor, found a way around it, and the corrected proof was published in 1995. The episode is often told as a story of genius; it is equally a story of writing and reading — of a proof set out clearly enough for a careful reader to find the one place where it did not hold.

Every proof has a reader: a referee, a student, a collaborator, your future self, and increasingly a proof assistant. Mathematical writing is the craft of making their job possible. It is not decoration added after the mathematics is done. Choosing what to define, what to name, which hypothesis to state and how to order the steps is part of understanding the mathematics — and writing it down is how mathematicians most often discover that they have not.

This lesson assumes you can already write proofs by the standard methods (see proof techniques). It is about writing them well.

A careful reader asks three questions of every sentence:

1. What does this mean? Every symbol, word and piece of notation must already have been given a meaning — by a definition, by a stated convention, or by a standard usage that the reader can identify.
2. Why is this true? Every claim needs a reason: an earlier step, a hypothesis, a cited result, or a computation the reader can redo.
3. What is its status? Is this a hypothesis, a definition, a proved result, a result proved elsewhere, a conjecture, a heuristic, a numerical observation?

Good mathematical writing answers these questions before the reader has to ask them. Most of the advice in this lesson is a consequence: define before use, state hypotheses, signpost the structure of proofs, cite precisely, label the status of every claim. The guiding image, from the knowledge graph of this curriculum: a proof is written for a reader who will check it against the stated hypotheses.

The status of a claim should never be left to the reader to guess. In this lesson we use four labels: proved (a proof is given here), cited (a proof exists in an identified reference), conjectured (no proof is known), and evidence (supported by computation or heuristics, not proved). The Lumenary labels its own content in the same spirit — "formally verified", "computationally tested", "ai-drafted" — and derives the first two from build reports rather than writing them by hand.

Conventions in definitions. In a definition, "if" means "if and only if": "an integer is even if it is divisible by $2$" defines evenness completely. In theorems, "if" means only "if". Writing "iff" in a theorem, and plain "if" in a definition, is the standard convention; some writers prefer to say "if and only if" everywhere, which is never wrong.

1. Define every symbol before you use it — and say what kind of object it is. Not "$x^2 = 4$ implies $x = 2$", but "if $x$ is a natural number with $x^2 = 4$, then $x = 2$". The type of $x$ is part of the statement: for integers it is false ($x = -2$). "Standard" notation is defined too, at least once: $\N$ contains $0$ in some books and not in others; $\subset$ means "subset" for some authors and "proper subset" for others; $\log$ is base $e$, $10$ or $2$ depending on the field.

2. State every hypothesis, in the statement. A theorem should be checkable from its statement alone. "If $a \mid bc$ then $a \mid b$ or $a \mid c$" is false ($6 \mid 4 \cdot 9$); it becomes Euclid's lemma when you add "where $a$ is prime". A hypothesis that appears only in the middle of the proof ("since $f$ is continuous…") is a hypothesis the reader did not know they were granting.

3. Make the order of quantifiers unmistakable. "For every $\varepsilon > 0$ and every $x$ there is $\delta > 0$ with …" (continuity) and "for every $\varepsilon > 0$ there is $\delta > 0$ such that for every $x$ …" (uniform continuity) differ only in word order. Prose such as "$|f(x) - f(y)| < \varepsilon$ for all $x$ when $|x - y| < \delta$ for some $\delta$" is ambiguous. When in doubt, write the quantifiers in front, in order.

4. Do not start a sentence with a symbol, and separate formulas by words. "$p$ is odd" after a full stop reads as a continuation; write "The prime $p$ is odd". "Since $n > 2$, $n^2 > 4$" runs two formulas together; write "Since $n > 2$, we have $n^2 > 4$." Logical symbols ($\forall$, $\Rightarrow$, $\therefore$) belong in formulas, not as abbreviations in prose.

5. Signpost the structure of every proof. Announce the method and the plan: "We argue by contradiction." "We proceed by induction on $n$." "It suffices to show that …" "There are two cases." Name intermediate claims ("Claim 1") and say when each is finished. A reader who knows where the proof is going can check each step against its purpose.

6. Give reasons, not reassurances. "Clearly", "obviously" and "it is easy to see" assert that a step is easy without making it so; if the step is easy, a short reason costs little, and if it is not, the word hides a gap. Keep "clearly" for steps that really are immediate, and even then prefer the reason.

7. Cite precisely. "By a theorem of Dirichlet" is not enough; write "by Dirichlet's theorem on primes in arithmetic progressions (Apostol, Introduction to Analytic Number Theory, 1976, Chapter 7)", or better, give the theorem number in the edition you used. The reader must be able to find the result and check that its hypotheses hold in your situation.

8. Use one symbol for one thing, and one name for one idea. Do not let $n$ be a natural number on one page and the dimension on the next; do not call the same object a "map", a "function" and a "transformation" in successive paragraphs, which suggests three different things. Choose suggestive notation ($\varepsilon$ small, $i, j$ indices, $G$ a group) and keep it.

9. Follow definitions with examples and non-examples. After defining a group, show $\Z$ under addition and say why $\N$ is not one. A non-example that just fails the definition shows which clause matters.

10. Label the status of every claim. Theorem or conjecture? Proved here, or cited? Proved for all $n$, or checked numerically for $n \le 10^6$? A theorem that depends on an unproved conjecture is a conditional theorem and must say so ("Assuming the generalised Riemann hypothesis, …").

A short proof is not always a clear one. Compression removes the signposts. The ideal is the shortest proof in which every step can be checked by the intended reader — which for a textbook is longer than for a research paper, and longer still for a proof assistant.

Much ambiguity in mathematical prose comes from conditionals. "$P$ only if $Q$" means $P \to Q$ ($Q$ is necessary for $P$); "$P$ if $Q$" means $Q \to P$ ($Q$ is sufficient for $P$). Compare a statement with its converse:

Then try ~q -> ~p (the contrapositive, equivalent to p -> q) and ~p -> ~q (the inverse, equivalent to the converse). A proof of "$P$ if and only if $Q$" must establish both directions, and good writing labels them: "($\Rightarrow$) Suppose $P$ … ($\Leftarrow$) Conversely, suppose $Q$ …".

Euclid's theorem, and a famous misstatement

Here is a version of Euclid's proof that appears in many places:

There are infinitely many primes. For suppose there were finitely many, $p_1, \dots, p_k$. Then $N = p_1 p_2 \cdots p_k + 1$ is prime, since it is not divisible by any $p_i$, contradicting the assumption.

The conclusion is right but a sentence is wrong. "$N$ is prime" does not follow: $N$ is not divisible by any $p_i$, but it might be divisible by primes not in the list — except that, under the assumption, there are none. In the proof by contradiction the claim is harmless; read as a standalone fact ("the product of the first $k$ primes plus one is prime"), it is false:

Many students remember the false standalone version. A careful writer states exactly what is used, and can avoid contradiction altogether:

The improvements are worth naming: the statement says exactly what is proved, for every $n$; $N$ and $p$ are defined before use; the one fact used about $p$ (a smallest divisor greater than $1$ is prime) is justified; and nothing false is asserted along the way.

A divisibility proof

The draft below is correct in outline, but a reader would have to repair it.

Theorem. $n^2 - 1$ is divisible by $24$ for $p > 3$ prime. Proof. Clearly $p^2 - 1 = (p-1)(p+1)$. $p$ is odd so both factors are even, and one is divisible by $4$. One of $p - 1, p, p + 1$ is a multiple of $3$, so we are done.

Problems: the statement uses $n$ where it means $p$; two sentences begin with symbols; "clearly" decorates an identity that needs no comment; "one is divisible by $4$" is stated without reason; the key point — that the multiple of $3$ cannot be $p$ — is omitted; and the final combination of the factors $8$ and $3$ is left to the reader.

The revision is longer, and better: each paragraph has a stated purpose, every step has a reason, and every hypothesis ("prime", "greater than $3$") is visibly used. A good test of a proof is to ask where each hypothesis is used; a hypothesis that is never used signals either a stronger theorem or a gap.

Almost all mathematics is now typeset with Leslie Lamport's LaTeX, built on Donald Knuth's TeX. A minimal article with theorem environments:

\documentclass{article}
\usepackage{amsmath, amssymb, amsthm}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\theoremstyle{remark}
\newtheorem{remark}[theorem]{Remark}

\newcommand{\N}{\mathbb{N}}               % one definition, used everywhere
\newcommand{\abs}[1]{\left\lvert #1 \right\rvert}

\begin{document}
\section{Primes}
\begin{definition}\label{def:prime}
A natural number $p \ge 2$ is \emph{prime} if its only positive
divisors are $1$ and $p$.
\end{definition}

\begin{theorem}[Euclid]\label{thm:euclid}
For every $n \in \N$ there is a prime $p > n$.
\end{theorem}

\begin{proof}
Let $N = n! + 1$ \dots
\end{proof}

By Theorem~\ref{thm:euclid}, \dots
\end{document}

Habits that make LaTeX serve the reader:

• Semantic macros. Define \N, \abs{x}, \norm{v} once with \newcommand. Notation stays consistent, and changing it later is one edit.
• Labels, not numbers. Refer with \label, \ref and \eqref (or \cref from the cleveref package); never type "Theorem 3.2" by hand. Use ~ before references so that they do not break across lines.
• Displays. Use \[ … \] or equation for a single displayed formula and align for chains of equalities aligned at =; number only the equations you refer to. Punctuate displayed formulas as part of the sentence.
• Words in formulas. Write \text{ for all } x, \operatorname{rank} and \sin, not for all x or rank in italic maths.
• Bibliography. Use BibTeX or BibLaTeX with full references (authors, title, journal or publisher, year), so that every citation is identifiable.

LaTeX checks syntax, not sense: a document can compile perfectly and still use an undefined symbol or cite a result whose hypotheses fail. The computation below shows what a mechanical checker can and cannot catch.

Suppose you are asked to write a three-page note explaining a theorem to fellow students. A structure that works:

1. What and why. State the main result early, informally first and then precisely, and say why it matters.
2. Setting. Definitions and notation, each with an example. Say which conventions you use ($0 \in \N$ or not).
3. Results. Lemmas building to the theorem, each labelled proved here, cited (with a precise reference) or conjectured.
4. Proofs. Signposted, with the main idea stated before the details. If a proof is omitted, say so and cite one.
5. Examples and limits. An example where the theorem applies; an example showing a hypothesis cannot be dropped.
6. Further reading. Where the reader goes next.

A status table at the start or end is a courtesy that formal projects make compulsory. For instance, for a note on the distribution of primes:

Large formalisation projects use blueprints — documents, often produced with Patrick Massot's leanblueprint tool, in which each informal statement is linked to its formal counterpart and the dependency graph is drawn with each node coloured by status. The Liquid Tensor Experiment (2020–22) and the formalisation of the polynomial Freiman–Ruzsa conjecture's proof (2023) were organised this way. The blueprint experiment below does a small version of the bookkeeping.

A proof assistant is an unforgiving reader: it accepts nothing that has not been defined, assumes nothing that has not been stated, and records the status of every claim. Formalising even small statements shows the principles above in action.

The domain is part of the statement (principle 1). The same sentence, about natural numbers and about integers:

/-- Over the natural numbers, `x² = 4` forces `x = 2`. (If `x ≥ 3` then `x² ≥ 9`; the cases
`x = 0, 1, 2` are checked one by one.) -/
theorem sq_eq_four_nat (x : ℕ) (h : x ^ 2 = 4) : x = 2 := by
  have hx : x ≤ 2 := by
    by_contra hc
    have h3 : 3 ≤ x := by omega
    have : 3 ^ 2 ≤ x ^ 2 := Nat.pow_le_pow_left h3 2
    omega
  interval_cases x <;> simp_all

/-- Over the integers the same sentence is false: `x = -2` is a counterexample. Writing
"if `x² = 4` then `x = 2`" without saying where `x` lives leaves the reader to guess which of
these two statements is meant. -/
theorem sq_eq_four_int : ¬ ∀ x : ℤ, x ^ 2 = 4 → x = 2 := by
  intro h
  have := h (-2) (by norm_num)
  norm_num at this

Quantifier order (principle 3). The same words in two orders, one true and one false:

/-- "For every number there is a bigger one": true (take `n + 1`). -/
theorem forall_exists_gt : ∀ n : ℕ, ∃ m : ℕ, n < m :=
  fun n => ⟨n + 1, Nat.lt_succ_self n⟩

/-- "There is a number bigger than every number": false (it would be bigger than itself).
The same words in a different order — so in prose, the order of "for every" and "there is"
must be unmistakable. -/
theorem not_exists_forall_gt : ¬ ∃ m : ℕ, ∀ n : ℕ, n < m :=
  fun ⟨m, hm⟩ => lt_irrefl m (hm m)

Hypotheses (principle 2). Euclid's lemma fails without primality; with it, it is in Mathlib:

/-- Without primality, "if `a ∣ bc` then `a ∣ b` or `a ∣ c`" is false: `6 ∣ 4 · 9`, but `6` divides
neither `4` nor `9`. -/
theorem dvd_mul_needs_prime : ¬ ∀ a b c : ℕ, a ∣ b * c → a ∣ b ∨ a ∣ c := by
  intro h
  have h' := h 6 4 9 (by norm_num)
  revert h'
  decide

/-- **Euclid's lemma**, with its hypothesis: if a prime divides a product, it divides a factor.
This applies Mathlib's `Nat.Prime.dvd_mul`. -/
theorem euclid_lemma {p a b : ℕ} (hp : p.Prime) (h : p ∣ a * b) : p ∣ a ∨ p ∣ b :=
  hp.dvd_mul.1 h

A structured proof. Theorem 1, written so that the comments are the proof's signposts; and the same theorem from Mathlib:

/-- **Euclid's theorem, written with its structure visible.** For every `n` there is a prime
`p > n`.

*Proof.* Let `N = n! + 1`. Since `N ≥ 2`, it has a smallest prime factor `p`. Suppose, for a
contradiction, that `p ≤ n`. Then `p ∣ n!`, and `p ∣ N`, so `p ∣ N - n! = 1`, which is impossible
for a prime. Hence `p > n`. ∎

Note what the proof does **not** claim: `N` itself need not be prime. -/
theorem exists_prime_gt (n : ℕ) : ∃ p, n < p ∧ p.Prime := by
  -- Step 1: `N = n! + 1` is not `1`, so its smallest prime factor `p` is prime.
  have hN : n.factorial + 1 ≠ 1 := by
    have := Nat.factorial_pos n
    omega
  have hprime : (n.factorial + 1).minFac.Prime := Nat.minFac_prime hN
  refine ⟨(n.factorial + 1).minFac, ?_, hprime⟩
  -- Step 2: suppose `p ≤ n`, for a contradiction.
  by_contra hle
  have hle' : (n.factorial + 1).minFac ≤ n := by omega
  -- Step 3: then `p` divides both `n!` and `n! + 1`, hence divides `1`.
  have h1 : (n.factorial + 1).minFac ∣ n.factorial := Nat.dvd_factorial hprime.pos hle'
  have h2 : (n.factorial + 1).minFac ∣ n.factorial + 1 := Nat.minFac_dvd _
  have h3 : (n.factorial + 1).minFac ∣ 1 := (Nat.dvd_add_right h1).1 h2
  -- Step 4: but a prime does not divide `1`.
  exact hprime.one_lt.ne' (Nat.dvd_one.1 h3)

/-- The same theorem from Mathlib, `Nat.exists_infinite_primes` (with `≤` rather than `<`). -/
theorem exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ p.Prime :=
  Nat.exists_infinite_primes n

The misstatement refuted:

/-- **The common misstatement is false.** A frequently written version of Euclid's proof claims
that "the product of the first `k` primes, plus one, is prime". It is not:
`2 · 3 · 5 · 7 · 11 · 13 + 1 = 30031 = 59 · 509`. The correct claim is that this number has a
prime factor outside the list. -/
theorem primorial_plus_one_not_prime :
    2 * 3 * 5 * 7 * 11 * 13 + 1 = 59 * 509 ∧ ¬ Nat.Prime (2 * 3 * 5 * 7 * 11 * 13 + 1) := by
  constructor
  · norm_num
  · norm_num

Status (principle 10). In Lean an unproved claim can be written with sorry, and the system then reports that the declaration depends on it — the formal equivalent of an honest "this step is not yet proved". This curriculum's main library forbids sorry, so a conjecture is recorded as a definition of a proposition, which asserts nothing, while what has actually been proved — a finite range — is a separate theorem:

/-- **Goldbach's conjecture**, *stated* but not asserted: every even number greater than `2` is a
sum of two primes. Making it a `def … : Prop` records the statement precisely while claiming
nothing about its truth — the formal counterpart of writing "Conjecture" rather than "Theorem". -/
def GoldbachConjecture : Prop :=
  ∀ n : ℕ, 2 < n → Even n → ∃ p q : ℕ, p.Prime ∧ q.Prime ∧ p + q = n

/-- **What is actually proved: a finite range.** Every even `n` with `2 < n ≤ 60` is a sum of
two primes, checked by computation (`decide`). This is evidence for the conjecture, and a
theorem about these finitely many cases — nothing more. -/
theorem goldbach_up_to_60 :
    ∀ n : ℕ, 2 < n → n ≤ 60 → Even n → ∃ p q : ℕ, p.Prime ∧ q.Prime ∧ p + q = n := by
  have key : ∀ n < 61, 2 < n → n % 2 = 0 →
      ∃ p < n, Nat.Prime p ∧ Nat.Prime (n - p) := by
    decide
  intro n h2 h60 heven
  obtain ⟨p, hpn, hp, hq⟩ := key n (by omega) h2 (Nat.even_iff.1 heven)
  exact ⟨p, n - p, hp, hq, by omega⟩

What formalisation does not do is write well for humans. Lean proofs can be as opaque as the worst prose; the comments, names and structure that make the proof above readable were choices. And what is not formalised here is everything about writing that has no truth value: clarity, motivation, examples, the order of ideas.

Some faults are mechanical enough for a program to find. The first program lints a draft and a revision of the divisibility proof above, as LaTeX: unbalanced environments, references to missing labels, undefined macros, sentences beginning with formulas, and words like "clearly".

r"""A small LaTeX linter: the mechanical part of careful writing.

Some writing faults are mechanical enough for a program to find. This linter
reads a LaTeX fragment and reports:

* environments that are opened and never closed (or closed out of order);
* \ref and \eqref to labels that do not exist;
* macros that are used but neither standard nor defined by \newcommand;
* sentences that begin with a formula (hard to read: "$n$ is prime" after
  a full stop looks like a continuation);
* words that assert ease instead of giving a reason ("clearly", "obviously").

We lint a draft paragraph and its revision. The checks are exact for the text
given, but they are heuristics about style: they find no mathematical errors,
and a clean report does not mean the writing is good.
"""

import re

#: Commands a document with amsmath and amsthm may use without defining them.
STANDARD = {
    "begin", "end", "label", "ref", "eqref", "cite", "emph", "textbf", "frac",
    "mathbb", "mathrm", "sum", "prod", "le", "ge", "ne", "in", "cdot", "dots",
    "ldots", "mid", "nmid", "equiv", "pmod", "bmod", "to", "mapsto", "infty",
    "alpha", "beta", "gamma", "delta", "varepsilon", "lambda", "pi", "sqrt",
    "left", "right", "quad", "qquad", "text", "newcommand", "section",
    "subsection", "item", "forall", "exists", "neg", "wedge", "vee", "sim",
    "binom", "lfloor", "rfloor", "colon", "subseteq", "cup", "cap", "setminus",
    "gcd",
}
STYLE_WORDS = ("clearly", "obviously", "trivially", "it is easy to see")

DRAFT = r"""
\begin{theorem}\label{thm:main}
$n^2-1$ is divisible by $24$ for $p>3$ prime.
\end{theorem}
\begin{proof}
Clearly $p^2 - 1 = (p-1)(p+1)$. $p$ is odd so both factors are even, and
one is divisible by $4$. One of $p-1,p,p+1$ is a multiple of $3$, so we are
done by Lemma~\ref{lem:three} and \Ztwo-arguments.
\end{theorem}
"""

REVISION = r"""
\newcommand{\Z}{\mathbb{Z}}
\begin{lemma}\label{lem:three}
Among any three consecutive integers, exactly one is divisible by $3$.
\end{lemma}
\begin{theorem}\label{thm:main}
If $p > 3$ is prime, then $24 \mid p^2 - 1$.
\end{theorem}
\begin{proof}
Write $p^2 - 1 = (p - 1)(p + 1)$. Since $p$ is odd, $p - 1$ and $p + 1$
are consecutive even numbers, so one of them is divisible by $4$ and
$8 \mid p^2 - 1$. By Lemma~\ref{lem:three}, one of $p - 1, p, p + 1$ is
divisible by $3$; it is not $p$, since $p > 3$ is prime. Hence
$3 \mid p^2 - 1$, and as $\gcd(3, 8) = 1$, we get $24 \mid p^2 - 1$
in $\Z$.
\end{proof}
"""

def environment_problems(text):
    """Unclosed or mismatched \\begin/\\end pairs."""
    stack, problems = [], []
    for kind, name in re.findall(r"\\(begin|end)\{(\w+)\}", text):
        if kind == "begin":
            stack.append(name)
        elif not stack or stack[-1] != name:
            opened = stack[-1] if stack else "nothing"
            problems.append(f"\\end{{{name}}} closes {opened}")
            if stack:
                stack.pop()
        else:
            stack.pop()
    problems += [f"\\begin{{{name}}} never closed" for name in stack]
    return problems

def missing_labels(text):
    """References whose label is not defined in the text."""
    labels = set(re.findall(r"\\label\{([^}]*)\}", text))
    refs = re.findall(r"\\(?:eq)?ref\{([^}]*)\}", text)
    return sorted({r for r in refs if r not in labels})

def undefined_macros(text):
    """Macros used but neither standard nor defined with \\newcommand."""
    defined = set(re.findall(r"\\newcommand\{\\(\w+)\}", text))
    used = set(re.findall(r"\\([A-Za-z]+)", text))
    return sorted(used - STANDARD - defined)

def sentences_starting_with_math(text):
    """Sentences beginning with $ (after . ! ? or at the start of an
    environment); line breaks inside a paragraph are ignored."""
    body = re.sub(r"\\(begin|end)\{\w+\}(\\label\{[^}]*\})?", ". ", text)
    body = " ".join(body.split())
    return len(re.findall(r"[.!?]\s+\$", body))

def style_flags(text):
    lower = text.lower()
    return [w for w in STYLE_WORDS if w in lower]

def report(name, text):
    lines = [f"{name}:"]
    checks = [
        ("environments", environment_problems(text)),
        ("missing labels", missing_labels(text)),
        ("undefined macros", ["\\" + m for m in undefined_macros(text)]),
        ("style words", style_flags(text)),
    ]
    for title, found in checks:
        lines.append(f"  {title:<17} {', '.join(found) if found else 'none'}")
    lines.append(f"  {'formula-initial':<17} {sentences_starting_with_math(text)}"
                 " sentence(s)")
    return lines

def main():
    for line in report("Draft", DRAFT) + [""] + report("Revision", REVISION):
        print(line)
    print()
    print("Not detected by any linter: the draft's theorem says n where it")
    print("means p, and its proof never explains why the multiple of 3 is not")
    print("p itself. Only a careful reader (or a proof assistant) catches that.")
    print()
    print("Epistemic status: exact pattern matching on the two fragments shown.")
    print("The checks are heuristics about mechanics and style; a clean report")
    print("says nothing about whether the mathematics is correct or clear.")

if __name__ == "__main__":
    main()

Notice what it does not find: the wrong variable in the draft's statement, and the missing argument that the multiple of $3$ is not $p$. Those need a reader.

The second program checks the logical bookkeeping of a short note: its items, their dependencies, and their statuses. It finds a forward reference, a valid order of presentation, results that are only conditional because they depend (perhaps indirectly) on a conjecture, and, in a second draft, circular reasoning.

"""A blueprint checker: order, circularity and the status of every claim.

A mathematical paper is a network of definitions and results, each used by
later ones. Formalisation projects record this as a "blueprint": a
dependency graph in which every node carries a status - proved here, cited
from the literature, or conjectured. This program checks a small blueprint:

* does the order of presentation ever use an item before it is stated?
* is there a valid order at all, or is the reasoning circular?
* which results are unconditional, and which silently depend on a
  conjecture (and so are only conditional theorems)?

The example is the skeleton of a short expository note; one result
in it rests on a conjecture, and a second version contains a circularity.
The analysis is exact for the data given; it cannot judge whether the
individual proofs are correct.
"""

import textwrap

#: (label, kind, status, uses), in the order the draft presents them.
DRAFT = [
    ("Def 1", "definition", "definition", []),
    ("Thm 3", "theorem", "proved", ["Def 1", "Lem 2"]),
    ("Lem 2", "lemma", "proved", ["Def 1"]),
    ("Thm 4", "theorem", "cited", ["Def 1"]),
    ("Conj 5", "conjecture", "conjectured", ["Def 1"]),
    ("Cor 6", "corollary", "proved", ["Thm 3", "Thm 4"]),
    ("Prop 7", "proposition", "proved", ["Conj 5", "Lem 2"]),
    ("Cor 8", "corollary", "proved", ["Prop 7"]),
]

def forward_references(items):
    """Pairs (item, dependency) where the dependency is stated later."""
    position = {label: i for i, (label, *_rest) in enumerate(items)}
    return [(label, dep) for i, (label, _, _, uses) in enumerate(items)
            for dep in uses if position[dep] > i]

def topological_order(items):
    """A presentation order respecting all dependencies (stable), or None
    if the dependency graph has a cycle."""
    remaining = {label: set(uses) for label, _, _, uses in items}
    order = []
    while remaining:
        ready = [label for label, *_ in items
                 if label in remaining and not remaining[label]]
        if not ready:
            return None
        first = ready[0]
        order.append(first)
        del remaining[first]
        for deps in remaining.values():
            deps.discard(first)
    return order

def find_cycle(items):
    """Some cycle of dependencies, as a list of labels, or None."""
    uses = {label: deps for label, _, _, deps in items}
    state = {}

    def visit(node, path):
        state[node] = "active"
        for dep in uses[node]:
            if state.get(dep) == "active":
                return path[path.index(dep):] + [dep]
            if dep not in state:
                cycle = visit(dep, path + [dep])
                if cycle:
                    return cycle
        state[node] = "done"
        return None

    for label in uses:
        if label not in state:
            cycle = visit(label, [label])
            if cycle:
                return cycle
    return None

def standing(items):
    """For each label: 'unconditional', 'conjecture', or 'conditional on X'.

    A proved result is only as strong as everything it uses."""
    info = {label: (status, uses) for label, _, status, uses in items}
    memo = {}

    def conditions(label):
        if label not in memo:
            status, uses = info[label]
            found = {label} if status == "conjectured" else set()
            for dep in uses:
                found |= conditions(dep)
            memo[label] = found
        return memo[label]

    out = {}
    for label, _, status, _ in items:
        if status == "conjectured":
            out[label] = "conjecture (stated, not proved)"
        else:
            conds = sorted(conditions(label))
            out[label] = ("conditional on " + ", ".join(conds)) if conds \
                else "unconditional"
    return out

def main():
    print("Draft order:", ", ".join(label for label, *_ in DRAFT))
    for item, dep in forward_references(DRAFT):
        print(f"  forward reference: {item} uses {dep}, which is stated later")
    print("A valid order:", ", ".join(topological_order(DRAFT)))
    print()
    print("Status of each item:")
    marks = standing(DRAFT)
    for label, kind, status, _ in DRAFT:
        print(f"  {label:<7} {kind:<12} {status:<12} -> {marks[label]}")
    print()
    circular = DRAFT + [("Lem 9", "lemma", "proved", ["Cor 10"]),
                        ("Cor 10", "corollary", "proved", ["Lem 9", "Thm 3"])]
    print("Second draft with two new items, Lem 9 and Cor 10:")
    print(f"  valid order exists: {topological_order(circular) is not None}")
    print(f"  circular reasoning: {' -> '.join(find_cycle(circular))}")
    print()
    print(textwrap.fill(
        "Epistemic status: an exact analysis of the dependency data as "
        "written. It finds forward references, circularity and hidden "
        "dependence on a conjecture, but it cannot tell whether any "
        "individual proof is correct, or whether the declared dependencies "
        "are complete - that is the reader's (or a proof assistant's) job.",
        width=78,
    ))

if __name__ == "__main__":
    main()

Both analyses are exact for the text and data given, and both are blind to the content of the proofs. That division of labour — machines for bookkeeping, readers (and proof assistants) for correctness — is the realistic picture.

• Definitions, postulates, propositions. Euclid's Elements (c. 300 BCE) fixed a format still recognisable in every textbook: definitions and postulates first, then propositions, each stated, proved and concluded ("which was to be demonstrated", later abbreviated QED).
• Commentary as proof. In China, Liu Hui's commentary of 263 CE on the Nine Chapters on the Mathematical Art supplied justifications for the book's procedures. In India, the concise verse of works such as Āryabhaṭa's Āryabhaṭīya (499) was accompanied by prose commentaries with explanations and demonstrations (upapatti); the Malayalam Yuktibhāṣā of Jyeṣṭhadeva (c. 1530) gives detailed proofs of the infinite series of the Kerala school.
• From words to symbols. Muḥammad ibn Mūsā al-Khwārizmī's algebra (c. 820) was written entirely in words. Symbolic notation developed over centuries — Robert Recorde's equals sign (1557), Viète's letters (1591), Descartes's $x, y, z$ (1637), Leibniz's $dx$ and $\int$ (1675), and Euler's $f(x)$, $\Sigma$ and $i$ in the 18th century.
• Rigour and style. The 19th-century arithmetisation of analysis made $\varepsilon$–$\delta$ writing standard. From 1935 the Bourbaki group wrote mathematics in a deliberately uniform, definition–theorem–proof style that shaped textbooks for decades. Paul Halmos's essay "How to write mathematics" (1970) and the 1973 AMS collection with Steenrod, Schiffer and Dieudonné made writing advice part of the profession.
• Typesetting and sharing. Donald Knuth created TeX between 1977 and 1978, and Leslie Lamport's LaTeX followed in the early 1980s; the arXiv preprint server (1991) made LaTeX the common language of mathematical publication. Since 2020, blueprints linking informal and formal mathematics have become the working documents of large formalisation projects.

• Paul R. Halmos, "How to write mathematics", L'Enseignement Mathématique (1970) — short, opinionated and still the best start.
• Donald E. Knuth, Tracy Larrabee and Paul M. Roberts, Mathematical Writing (1989) — notes from Knuth's Stanford course, with many before-and-after examples.
• Nicholas J. Higham, Handbook of Writing for the Mathematical Sciences (2nd edition 1998; 3rd edition 2020) — comprehensive and practical, including LaTeX.
• Norman E. Steenrod, Paul R. Halmos, Menahem M. Schiffer and Jean A. Dieudonné, How to Write Mathematics (1973).
• Steven G. Krantz, A Primer of Mathematical Writing (1997; 2nd edition 2017).
• Leslie Lamport, LaTeX: A Document Preparation System (2nd edition 1994).
• Imre Lakatos, Proofs and Refutations: The Logic of Mathematical Discovery (1976).
• Daniel J. Velleman, How to Prove It (1994; 3rd edition 2019) — for the structure of proofs.

Next steps in the Lumenary: reading the mathematical literature, research ethics and attribution, and formalising published mathematics.