Review: surveys, seminal works, forward citations

Grades: measured (controlled study or corpus count), supported with caveat, convention, untested.

Grey sources (guides, handouts, blogs, Q/A, project documentation) are scored on 20 criteria in sources.md. A source scored below 10 is marked "example only": the row shows a practice, and no claim rests on it.

0. Existing reviews

Searched first (protocol.md 3). None of them reviews the layout of a research article or of a proof for its reader.

Review What it covered How this review differs
Stylianides 2024 Systematic review of 103 papers on proof and proving, school and university (abstract read) Sorts papers by teacher, student and content; this review asks only how a text should be laid out
Stylianides 2017 Handbook chapter: proving as problem solving, as convincing, as social; discusses Hodds 2014 and why mathematicians read proofs (read in part) Narrative, argues for intervention studies; this review compares layouts
Lessing 2025 Systematic review of reasoning and proof in mathematics education (full text read: 80 publications, 2019 to 2024) Broad scope; no layout question
Teledahl 2024 Systematic review of 48 works on quality in students' mathematical writing: proof writing shows a common set of standards, such as defining assumptions and variables (abstract read) Students' written proofs; this review looks at what readers of papers meet
Powell 2017 Synthesis of 29 studies of mathematics writing, grades 1 to 12, 1991-2015 (abstract: 29 studies, grades 1 to 12, 1991 to 2015) School writing, not research articles
Tran Minh 2025 Narrative survey of proof assistants used for teaching (abstract read) Teaching tools; this review's formal strand is the blueprint as explicit structure
Mejia-Ramos and Inglis 2009 Found little work on how students read proofs, as against how they construct them (secondary, from Davies 2021) Not opened; the gap it names is the one strand 5 fills

Finding: this search did not find a review of how mathematicians read research papers, or of article layout.

0a. Surveys that hand over the map

Survey What it maps
Knuth 1989 Transcripts of a 1987 Stanford course with guest lectures by Halmos and Lamport; names the earlier classics, Gillman 1987 among them
Hanna & de Villiers 2012 The ICMI study on proof in education: functions of proof, proof and explanation, generic proof
Alcock 2015 One research programme on proof reading in three stages: e-Proofs, eye movements, self-explanation
Bayer 2022 Mathematicians and formal-proof researchers on the gap between proof in theory and in practice

1. Style guides: what mathematicians advise

Source Advice on structure Grade
Halmos 1970 Organisation is a tree, almost never a chain; motivation first, then the statement, then the proof convention, untested
Halmos 1970 A theorem is one short sentence; a proof repeated twice signals a missing lemma convention, untested
Knuth 1989 A theorem statement stands alone, without leaning on assumptions in the preceding text convention, untested
Knuth 1989 Proofs carry signposts, such as "we divide the proof into two parts" convention, untested
Krantz 2017 Section 1 summarises the main results in plain words, then history, then the paper's plan convention, untested
Krantz 2017 Section 2 gives definitions and formal statements; Section 3 the big steps; lemma details go last convention, untested
Krantz 2017 Rule of thumb: of readers who read the abstract, 20% read the introduction and a quarter of those the body convention, untested
Higham 2020 Plan the high-level organisation early and rank the contributions (secondary, read in a summary of the 2nd edition) convention, untested
Tao 2026a The introduction states the main results, or an informal version labelled as such, compares with prior work, and outlines the proof convention, untested
Tao 2026b Milestones are self-contained propositions stated early; each lemma sits near its use convention, untested
Tao 2026b Draw a box per lemma and an arrow per dependency to find the sections convention, untested
Tao 2026d A paper split into lemmas survives one failed lemma; a global error is found by skimming the structure convention, untested
Serre 2003 The talk targets local language faults (articles, unnamed maps), not section structure (secondary; example only, not viewed) convention, untested
Gillman 1987 Listed by Knuth 1989 as a standard manual; not read for this review not graded

The guides disagree among themselves: Halmos 1970 quotes one adviser who praises chains of lemmas and another who finds them boring.

2. The template: genre analysis and publisher rules

Source Finding Grade
Graves 2013 30 pure and applied articles follow Introduction-Results, with no Methods or Discussion section measured, descriptive
Kuteeva 2015 22 pure articles plus author interviews: three compulsory stages, Openings, Proofs, Endings, and an optional post-introduction measured, descriptive
Kuteeva 2015 All but one of the 22 announce the principal findings in the opening measured, descriptive
Kuteeva 2015 17 of 22 have a separate background or notation section; 11 of 22 have no conclusion measured, descriptive
Kuteeva 2015 Some form of Move 2 (niche) appears in 10 of 22 introductions: 4 raise a question, 6 state a gap (sum of two counts) measured, descriptive
Graves 2014 Introductions establish presumptions such as definitions before results (secondary) supported with caveat
AMS 2017 AMS journals require an abstract without citations; the AMS proceedings checklist suggests at most about 150 words for short papers and 300 for long ones convention; no citations enforced by the publisher, length only suggested
AMS 2017 At least one primary MSC code is required; keywords are optional; theorem styles are plain, definition, remark convention, enforced by the publisher
arXiv 2026 Abstracts over 1920 characters are refused; mathematics has an optional MSC-class field (example only: the page is the platform's statement about its own server) convention, enforced by the server
EMS 2026 EMS Press: abstract brief, self-contained, no citations like "[5]", no displayed formulas; theorem styles plain and definition; no guidance on the introduction convention, enforced by the publisher
LMS 2021 Journal of the LMS: every article needs a stand-alone abstract; at least 18 pages; no rule on how proofs are laid out convention, enforced by the publisher

The societies and publishers regulate form (abstract, theorem styles, length) and leave the layout of introductions and proofs to authors.

3. The DTP style and its critics

Source Claim Grade
Thurston 1994 Names the DTP model and argues it omits where questions come from and how understanding is passed on supported with caveat
Thurston 1994 An idea told one-on-one in minutes becomes an hour's talk and a 15 to 20 page paper; channels narrow at each step supported with caveat
Jaffe 1993 The paper Thurston answered: speculation should be labelled apart from proved results convention, untested
Weber 2004 Case study of one professor teaching real analysis in DTP lectures (secondary) supported with caveat
Dreyfus 1999 Students rarely meet the kinds of knowledge that proving needs, including what counts as an explanation (secondary) supported with caveat
Hanna 1990 Separates proofs that only prove from proofs that also explain convention, untested
Lew 2019 Students did not know language conventions that mathematicians took for granted, such as how objects are introduced measured, qualitative

4. Structured and calculational proofs

Source Claim Grade
Leron 1983 Seminal: arrange a proof in levels, main ideas on top and details below, to communicate better convention, untested until Fuller 2014
Lamport 1995 Numbered hierarchical steps, each with its own proof, aimed at rigor rather than communication convention, untested
Lamport 1995 Rewriting conventional proofs in this form found serious errors in almost all of one co-authored paper's proofs supported with caveat (anecdote)
Lamport 2012 Readability and rigor are separate goals; about 4 to 10 steps per level reads best; step names past level 4 are hard to read convention, untested
Lamport 2012 A proof sketch may sit before any level, so a reader can stop at the sketch convention, untested
Dijkstra 1990 The calculational format: expression, relation, hint in braces, expression convention, untested
Gries 1993 A textbook built on calculational proofs for discrete mathematics convention, untested
van Gasteren 1990 A thesis on the shape of mathematical arguments from the same calculational school; not read for this review not graded
Back 2010 Structured derivations unify forward, backward and calculational styles, for secondary and university teaching convention, untested (its evaluations not read)
Herbst 2002 History of the school two-column proof: it fixed a format for proof and cost students' part in finding ideas supported with caveat

5. Empirical work on reading proofs

Source Design and result Grade
Mejia-Ramos 2012 Seven-dimension model: terms, logical status, justifications, high-level idea, modular structure, transfer, examples supported with caveat (model, built from interviews and surveys)
Mejia-Ramos 2017 Method to build short, reliable multiple-choice comprehension tests per proof measured
Inglis 2012 Eye tracking, 18 students and 12 mathematicians (secondary count): students dwell on formulae; experts look back between consecutive lines about three times as often measured
Weber 2013, Inglis 2013a Dispute over whether mathematicians skim a proof first contested
Weber 2008 8 mathematicians validating proofs use formal, informal and example-based reasoning measured, qualitative
Weber 2011 9 mathematicians read by authority, line by line, or by modules measured, qualitative
Mejia-Ramos 2014 Survey of 118 mathematicians on why and how they read proofs (secondary count) measured, survey
Inglis 2013b 109 mathematicians disagreed on whether one calculus proof was valid measured
Fuller 2014 Structured versus linear proof: structured readers better at picking a summary, somewhat worse on justifications, transfer and examples, mostly not significant measured, one study
Roy 2017b e-Proof (N = 21) versus textbook proof (N = 28): equal at once, e-Proof group retained less after two weeks; time by group F(1,47) = 5.659, p = .021 measured
Lew 2020 Generic versus traditional proof, randomised: no difference in comprehension, though students preferred generic measured
Hodds 2014 Self-explanation training before reading: d = 0.95 in Experiment 1, in the lab; a classroom study of 107 first-year students (Hodds 2014; Alcock 2015) found smaller effects, d = 0.41 immediately and d = 0.35 delayed measured
Davies 2020 Proof summaries scored by comparative judgement are reliable; top summaries name the logical structure measured
Weber 2015 Strategies of good student readers: try the proof first, find the framework, split into parts, test with examples (secondary) supported with caveat

6. Formal proofs as explicit structure (pointer only)

  • mathlib 2020: a library of formal mathematics in Lean, where every dependency is checked by machine.
  • leanblueprint (Massot 2026): a LaTeX outline in which each statement lists the labels it uses, from which a dependency graph is drawn and coloured by formal status.
  • Gowers 2023 and PFR: the Polynomial Freiman-Ruzsa proof was formalised through such a blueprint within weeks (Tao 2023).
  • Tao 2023: formalising surfaced missing hypotheses in the written proof, such as a set required to be nonempty.
  • leanblueprint: its README lists about 40 projects that use it and showed 394 GitHub stars when read (measured, descriptive; the count is the repository's own).
  • Mathlib 2026: every file opens with a module docstring (title, summary, main statements, notation, implementation notes, references); every definition and major theorem needs a docstring, and linters flag missing ones.
  • Uskuplu 2026: a preprint of a tool that draws the dependency graph from LaTeX with no formalisation; it reports no user study.