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.