Proof Readability

Author: Moran Koren, Ben-Gurion University of the Negev (korenmor@bgu.ac.il). Part of the Theorist Toolbox.

Proof readability

Relationship to proofread: proofread is a report-only, whole-paper prose checker (11 categories, never edits source). proof-readability edits in place, is proof-specific, runs only after a correctness gate, and holds a content-preservation invariant proofread does not. Audit a whole paper's prose → proofread; edit the exposition of a verified proof → proof-readability.

Edit verified proofs so a reader can follow them without reconstructing steps, chasing broken references, or decoding notation. This skill runs after a proof has been written (e.g., by math-proof) and after its correctness has been verified (by domain-reviewer, lean-check, or the user). It is an exposition pass, not a proving pass.

Position in the pipeline

math-proof  →  verification (domain-reviewer / lean-check / user)  →  proof-readability
   (correctness)              (acceptance)                  (exposition only)

The prime invariant: never change the mathematics. Every edit must be content-preserving — reorder, signpost, expand, annotate, rename consistently, fix references and typos. Do not strengthen, weaken, or "simplify" any claim; do not replace an argument with a different one; do not silently fill what you believe is a gap with new mathematics.

If you find an actual gap or error while editing, stop editing that proof and flag it. Report the suspect step precisely ("the inequality in Eq. (3) silently uses FOSD via Eq. (1); I cannot verify it from the stated assumptions") and route it back to the user (re-open the proof via math-proof, or verify the step via verify-math). A readability pass that quietly patches math defeats the verification that already happened.

Guiding principles

• Minimize the reader's work (Lee): every edit is judged by whether it reduces what the reader must reconstruct, look up, or hold in memory.
• Readers are human (Hwang): "We get tired, we forget, we skim when we should scan. Write accordingly." Judicious redundancy is expository error-correction, not padding; "mathematical prose should not be an access barrier a reader must overcome to prove their worthiness."
• The detail criterion (Lee): omit a step only if it would be obvious to this audience how to fill it in; if it wasn't obvious to the writer at first, something needs to be said. Aim for "just enough to give the reader the Aha! experience that makes the rest obvious."
• Be accurate even when imprecise (Hwang): informal glosses and intuition sentences must be literally defensible, not merely morally true.

The six-layer pass

Work through these layers in order. Layers 1–2 are structural (read the whole proof first); layers 3–6 are local.

Layer 1 — Architecture

• Three-layer presentation for main results. Main text: statement + short proof sketch + an intuition paragraph outside the proof environment ("The intuition behind this result is as follows…"). Formal proof in the appendix. State explicitly where each proof lives ("The proof of Proposition 3 is in Appendix C").
• Restate before proving. When a proof is deferred to an appendix, restate the result verbatim immediately before its proof. Open a proofs appendix with a notation-recap block (a short glossary plus the pre-derived equations the proofs reuse).
• Gloss-then-state. Precede every lemma with one or two plain-language sentences giving what it says and its role in the main proof: "The next lemma shows that the threshold is monotone in q; this is the engine of Theorem 2."
• Close composite proofs explicitly. When a theorem is assembled from lemmas, end with a wrap-up sentence — "Combining Lemmas 1, 2, and 5 establishes Theorem 2" — and a QED. The end of every proof must be unmistakable, so the reader needs no mental backtracking to confirm all obligations are discharged.
• Factor exact duplicates. "A lemma is to a proof what a subroutine is to an algorithm" (Hwang). If a long derivation is repeated with cosmetic substitutions (hats, bars, swapped indices), extract one symmetric lemma and instantiate it twice. (Coarser re-chunking of the lemma structure is a contested edit — see below.)
• Prose order = logical order, or motivate the inversion. Reorder so each statement follows from what immediately precedes it or from something much earlier — avoid jumping around. When a hard auxiliary lemma must be proved before its use, add a motivating sentence first, or its appearance "could seem arbitrarily magical."
• Self-contained statements. A lemma must be readable in isolation: restate the objects and quantifiers in the statement itself ("Let w ∈ W and let w′ be the η-coarse contract of Definition 3…"), never inherit them silently from a page of surrounding prose. No theorem statement may read as false in isolation because of an off-page standing convention; if hypotheses pile up, bundle them into a named definition ("a regular economy is one satisfying…").
• Labels signal role. Theorem = important result; Proposition = interesting but lesser; Lemma = a tool for proving something else; Corollary = follows easily from the preceding result. Check each label matches the result's role.

Layer 2 — Signposting

• Architecture opener. The first sentence of every proof states the method and plan: "The result is established in two steps: first we show X; then we use X to bound Y." "We prove the contrapositive." "By Lemma 2 it suffices to prove the claim for t′ = 1." Any non-direct method (contrapositive, contradiction, induction) must be declared within the first lines.
• Named steps for long proofs. Any proof over roughly half a page gets numbered or named steps, each opening with what it will show, and a closing recap reciting which step delivered which piece ("the first bound came from Step 1; the tighter bound from Steps 2–3").
• Roadmap counts must match the body. "We split the proof into three cases" followed by four cases, or step numbers that contradict the prose, is worse than no roadmap. Verify every announced count and every "by step 1" pointer.
• Enumerate cases up front. State all cases, confirm they are exhaustive and mutually exclusive, label them (Case I, Case II, … with explicit parameter ranges), then prove each.
• Mark where assumptions open and close (Gro-Tsen). "We temporarily assume x > 0. … This concludes the case x > 0." In a long case or induction, drop reminders: "still working under the assumption that x > 0," "recall the inductive hypothesis gives…". The structure must be visible even to a reader skipping the details.
• State the purpose of every assumption. Always "assume toward a contradiction that…" — never a bare assumption the reader can't classify as to-be-refuted versus a genuine case. Flag atypical branches: "we first handle the degenerate case where…".
• Goal statements before algebra. "It remains to show that w′(i) ≤ 2H." "We want to show the left-hand side is smaller than 1." The reader should know the destination before wading in.
• Meta-comments that don't participate in the logic (Abou Samra): announce the technique ("we construct A by diagonalizing over all strategies"), flag surprises ("we cannot apply Dijkstra's algorithm directly because…"), preempt natural questions ("one could show a₁ already works, but this argument is simpler"). Keep them to a sentence or two; longer asides move before or after the proof.

Layer 3 — Line-level justification

• Every assertion has a visible status (Sundstrom): assumption of the theorem, previous step of this proof, previously proved result, definition, axiom, or well-known background fact — these are the only legitimate justifications (Lee), and the reader must be able to tell which one each line uses. Omit the citation only when it is genuinely more effective unstated for this audience.
• Every inequality gets a named reason at the line where it occurs — an assumption, lemma, equation number, or one-clause argument ("by convexity of r⁻¹"). A trailing "where the second and third inequalities follow from…" clause is acceptable only if it covers every relation in the chain; an uncited step two displays later is the failure mode to hunt for.
• Every sign, monotonicity, or limit claim gets a one-clause justification. "The derivative is negative" → "negative, since each factor is positive and (2q−1) > 0." Bare declaratives like "the expression above is positive for every q" are the single most common stumbling block — expand each one or point it at a lemma.
• Instantiate cited theorems at the call site (Gro-Tsen): don't just write "by Theorem 3.1 of [12]" — say what each of the theorem's quantified variables is in the present context, like passing arguments to a function. When importing an external result, restate it in this paper's notation; cite with precise pointers ("[12, Theorem 3.1]", never "by [12]").
• Chain discipline (Lee): write a = b = c = d only when the steps are provable in the order shown; transitive relations may mix (a ≤ b = c < d) but never a ≤ b ≥ c, and never chain ≠. In displayed derivations, align the relation symbols vertically and do not repeat an unchanged side.
• Narrated algebra: one display per transformation, each prefaced by an active-voice sentence: "Rearranging, we get," "Factoring out common terms," "Substituting m̄ = αn," "As n → ∞, the second term vanishes, so". Break unbroken page-width algebra blocks into this rhythm.
• Expand compressed steps. "By plugging this into Definition 2 we get…" costs the writer one displayed line and saves every reader the reconstruction. Same for skipped telescoping sums, omitted LP solutions, and "which is simply…" closed forms: show one intermediate line or name the cancellation.
• Display and number key derived quantities. A formula that the proof leans on (a threshold, a cutoff, a closed form) must not arrive as a dense inline fraction; display it, number it if it is ever referenced again, and show the one-line derivation that produced it.

Layer 4 — Notation hygiene

• Dual-code definitions (Gro-Tsen): state each definition in symbols and in words — "let P := {x ∈ ℝ : x > 0} be the set of positive real numbers." The verbal gloss is an error-correcting code; "a misunderstood definition often makes all that follows unrecuperable."
• Define before use, once, in a visible place. Every symbol is either previously defined or quantified, at the latest within the sentence where it first appears (Lee). Proof-local objects (ad hoc sequences, mid-proof abbreviations like δ(μ, q, γ)) get an explicit displayed definition, ideally collected at the proof's start rather than minted mid-sentence.
• No notation dumps. Introducing four symbols at once followed by an asserted identity is the anti-pattern; introduce one symbol at a time with a purpose clause ("let η_q denote the contribution of high-signal players to the numerator").
• Restate object types and names on reuse (Wintz): "Thus, the vector x solves the optimization problem in (2)" beats "Thus, x solves (2)" — it saves the reader a back-search and avoids opening a sentence with a symbol. Likewise recall decorated notation at the point of use: when r̄ or J̄_B reappears pages after its definition — especially alongside its undecorated twin — append "(the ranking under truthful bidding)".
• Use descriptive names alongside numbers (mlk): "combining the monotonicity formula (7) with the reduction Lemma 3.13" — five extra words and the reader immediately feels what is going on, instead of cross-referencing three bare numbers.
• Naming hygiene (Rüping): keep names stable across sections (a group called G stays G); use parallel names for parallel objects (W ⊂ V and W′ ⊂ V′); never double-book a letter (k as field and as index); don't name what is used only once ("For every vector v…" needs no "Let V be a vector space" if V never recurs).
• Describe constructed objects in words, not encodings (Abou Samra): "the graph H obtained by removing vertex v from G," not H := (V_G∖{v}, {e ∈ E_G : v ∉ e}).
• Prefer unambiguous symbols: ⊆/⊊ over bare ⊂ where the convention is not fixed, ⌊x⌋ over [x], gcd(a, b) over (a, b).
• Audit consistency mechanically: argument orders of multi-argument functions (φ(γ, n, k) vs φ(γ, k, n)), ε vs ϵ, subscript slips (μ_n for μ_{t′}, s₂ for s₃), subsequences taken but never renamed (lim sup silently becoming lim), bounds that differ between a statement and its appendix restatement, variant spellings ("finite dimensional" vs "finite-dimensional").
• Abbreviate repeated parameter lists. After the first full appearance of x*(q_i, q_j, μ_i, μ_j, γ_i, γ_j), declare "we write x* for short" and use the short form; a monotonicity claim drowning in six-argument lists is unreadable.

Layer 5 — Intuition

• One intuition sentence after each key derivation, connecting the math to the model: "The threshold drops because no-votes carry less information, so fewer yes-votes suffice to outweigh them."
• An intuition paragraph after every main theorem, outside the proof environment, possibly with a concrete narrative (extreme cases, an Alice/Bob story, a toy example with a table).
• "In words" translations after dense formal statements: "In words, Corollary 1 states that if the price is moderate, the probability the campaign succeeds in state H approaches one."
• Provide what the reader would have to draw or compute (Latapy): if following the proof requires sketching a region, tabulating cases, or tracking a small example, supply the figure, table, or worked instance. After a long proof, consider a short walk-through on a concrete example.
• Keep intuition segregated from the formal argument — before the proof or after the QED, never interleaved with the algebra in a way that blurs what is proved versus what is motivated. Every informal gloss must be literally defensible (no "f(x′) is close to f(x)" when the true statement is a limit).

Layer 6 — Sentence and formula grammar

The line-by-line mechanics, mostly from Lee's Some Remarks on Writing Mathematical Proofs:

• Complete sentences in paragraphs. Every formula functions grammatically as a noun (an expression) or a clause (a relation, whose verb is the relation symbol); a formula cannot stand alone as a sentence. Sentences end with punctuation — including a period after a sentence-ending displayed equation.
• Never begin a sentence with a mathematical symbol. Reword: "f is continuous" → "The function f is continuous."
• Never let two formulas meet with only punctuation between them. "If x ≠ 0, x² > 0" → "If x ≠ 0, then x² > 0."
• Relation symbols connect formulas, never words. "a number that is > 2" is banned; write "a number greater than 2" or "a number x with x > 2."
• Logical symbols (∀, ∃, ⇒, ⇔, ∧, ∨, ∴) become English words in prose. "For every," "there exists," "implies." ⇒/⇔ are tolerated only between fully symbolic statements or statement labels ("we prove (a) ⇔ (b)"), never splicing English clauses.
• No blackboard abbreviations in formal text: "s.t.", "w.r.t.", "w.l.o.g.", "iff" — write them out. Use "i.e." and "e.g." correctly or not at all. Don't double a connective word with a symbol ("Since x ∈ V → x has a magnitude" uses two connectives for one).
• No computer notation: no * for multiplication, no ^ for powers, no slashed complex fractions — display them. Roman type for operator names (sin, log, gcd), italics for variables, consistent fonts (a symbol must look the same at every occurrence).
• No ambiguous pronouns (Hwang): every "it"/"this" has an unmistakable antecedent — "if you aren't sure what noun 'it' refers to, there is an important detail you don't understand."
• Prefer positive statements to negated ones (Wintz): "There is no solution x with x > 0" → "Every solution x satisfies x ≤ 0."
• Untangle "respectively" and parenthetical (resp.) constructions into serial clauses when they force the reader to zip two lists.
• Two read-tests:
  • Read-aloud test: expand each relation symbol to its verb phrase and check the sentence is grammatical ("let x < y be real numbers" fails — it reads "let x is less than y be real numbers").
  • Knuth's "blah" test: replace every formula with "blah" and check the surrounding prose still makes sense, because readers skim equations on a first pass. If the prose collapses, add connective words.