Protocol: how the pool of sources was built

This file records how the formal and grey sources of this review were searched, selected and scored, after Garousi 2019.

The method is a lighter multivocal literature review (see the evidence README). The formal pool was built before the protocol existed, and the grey search was run to the protocol. Dates of every search: 2026-10-28.

1. Why grey literature (Garousi 2019, Table 4)

# Question Answer for this topic
1 Is the subject complex and not solvable by the formal literature alone? No: the comprehension question is bounded and academic
2 Is there a lack of volume or quality of evidence in the formal literature? Yes: one randomised test of a structured proof, none of where the main theorem goes
3 Is contextual information important? Yes: conventions differ between pure and applied mathematics and between journals
4 Is the goal to validate scientific outcomes with practical experience? Yes: do the style guides' rules survive the comprehension studies?
5 Is the goal to challenge practice with research, or the reverse? Yes: Fuller 2014 and Roy 2017b against the guides
6 Would a synthesis help both communities? Yes
7 Is there a large volume of practitioner sources? No: a few dozen guides, which repeat one another

Five yes answers include grey literature. Garousi 2019 notes that bounded academic topics have little practitioner literature. The last answer confirms this, so the grey search is small.

2. Questions

Q1 to Q5 of frame.md:

  • Q1: section order;
  • Q2: place of the main results;
  • Q3: layout of one proof;
  • Q4: effect of layout on comprehension;
  • Q5: explicit dependencies between lemmas.

3. Existing reviews (Garousi Guideline 2)

Four searches, run first, on the web; results are placed in review.md strand 0.

Id String Found worth reading
E1 systematic review proof comprehension OR proof reading, undergraduate Stylianides 2024, Lessing 2025, Davies 2021 (cites a 2009 review, secondary)
E2 proof and proving literature review handbook chapter Stylianides 2017
E3 survey of proof assistants or interactive theorem provers, mathematicians' use Tran Minh 2025
E4 review of research on mathematical writing Teledahl 2024, Powell 2017

6. Stopping rule (Guideline 8)

Effort bounded: the top 10 results per string, nine web strings and four API queries fixed in advance, one level of snowball. Saturation was observed, not used as the rule: the last two included sources (Stanford 2023, EMS 2026) added no concept not already met. By contrast, Mathlib 2026 and Ilmavirta 2015 had each added one.

7. Selection

Include a source that answers Q1 to Q5 with a concrete layout rule or a measured fact, written by a mathematician or a body that publishes mathematics, and readable in full. Exclude pages that are unreachable, off the question, or copies of a source already held.

8. Quality of grey sources (Guideline 11, Table 7)

Twenty criteria scored 1, 0.5 or 0, in eight groups:

  • authority 4, methodology 6, objectivity 4, date 1
  • position among related sources 1, novelty 2, impact 1, outlet tier 1

Tier 1 scores 1 (books, publisher rules), tier 2 scores 0.5 (handouts, Q/A, repositories), tier 3 scores 0 (blogs). Impact is scored 0.5 when no count was taken.

Threshold 10 of 20: below it a source stays only as an example of practice. Scores are in sources.md.

9. Extraction and synthesis

Extracted per source: the rule or fact, its question, the stated limits. Synthesis is narrative by question, traceable through sources.md.

10. Limits

  • A second rater re-scored 5 of this topic's grey sources blind (method): 4 of 5 decisions agree. The Stanford proofwriting checklist scores 9.5 and 14.5, since the raters judged novelty against different things; it stays an example of practice.
  • Search engines personalise and change; the Tao pages show no date.
  • The OpenAlex counts came a day after the Semantic Scholar ones; the two indexes differ, so the counts are not comparable.
  • Higham 2020 and Serre 2003 were not read, only described by secondary sources.