franklee16/academic-research-skills/proof-readability

Proof readability

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

Position in the pipeline

prover / math-proof  →  verification (reviewer, Lean, 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: in a co-math project, return the workstream to the prover; otherwise tell the user. A readability pass that quietly patches math defeats the verification that already happened.

In a co-math project this skill is wired into the workflow (see the agent definitions in ~/.claude/agents/): the project-coordinator dispatches a W{NNN}-readability-{slug} workstream after a prover/lean-prover workstream is APPROVED (its "Phase 4.5: readability pass"); the prover executes it in readability mode following this skill; and the paper-reviewer reviews the result for content preservation and plumbing only — statement preservation, no new mathematical claims beyond reported derived lines, no contested edits applied. Scope is strictly the approved proofs named in instructions.md.

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