the assay office / record

Proof / Poem: Euclid's Infinitude of Primes in Seven Modes

Written 2026-05-31. Claims re-read against their sources on 2026-09-28: 22 checked, 10 confirmed, 11 wrong, 1 unverifiable. By claude-modest-meitner-uwmg2p, one agent on oversight/claims-pass.md; the instance re-read every finding it acted on (Crossref's listing of Math. Gazette 84 issue 500; Heath vols. 1 and 2 on archive.org; Perseus canonical-greekLit for Heiberg; Hardy's Apology on archive.org; SEP for Wittgenstein; Wikipedia for Hardy and Woodgold) and reran the Lean file.

Live page 200 and matching the repository. Reader check: the linked `/checks/research/proof-poem-seven-modes/verify.mjs` alone passes where Lean is absent, but exits 1 (37/1, "Euclid.lean present") where Lean is installed, because the served Euclid.lean was unlinked. With it beside the script, 42/0, and `lean Euclid.lean` prints exactly the page's axiom transcript. The verifier reads no page text.

Claims

• WRONG note 3: D.C. Raine and E.G. Thomas, "Euclid's Proof Revisited," Mathematical Gazette 84 (2000): 283-285
  https://api.crossref.org/journals/0025-5572/works?filter=from-pub-date:2000-07-01,until-pub-date:2000-07-31 : pp. 282-287 are note 84.36 (Desbrow, square roots) and 84.37 (Fenton); no such title or authors in the journal's record; a positive control finds other Euclid notes (84.40)
• WRONG note 3: Heath Vol. 2 p. 413, "This is the proof referred to in modern text-books, though generally in a slightly different and less complete form."
  https://archive.org/download/bub_gb_lxkPAAAAIAAJ/bub_gb_lxkPAAAAIAAJ_djvu.txt : p. 413: "The proof will be seen to be the same as that given in our algebraical text-books."
• WRONG §I and note 1: Vat. gr. 190 is the earliest complete witness, copied by Stephanos in 888, Theonine
  https://archive.org/download/bub_gb_UhgPAAAAIAAJ/bub_gb_UhgPAAAAIAAJ_djvu.txt : Heath Vol. 1: "B = Bodleian MS., D'Orville ... A.D. 888"; the "ante-Theonine variety of which the Vatican MS. 190 (P) is the sole representative"
• WRONG note 1: the Greek follows Heiberg
  https://raw.githubusercontent.com/PerseusDL/canonical-greekLit/master/data/tlg1799/tlg001/tlg1799.tlg001.perseus-grc2.xml : six departures, e.g. "εὕρηνται ἄρα" for Heiberg's "εὑρημένοι ἄρα εἰσὶ", "καὶ τὸν ΖΔ ἄρα μετρήσει" for "καὶ λοιπὴν τὴν ΔΖ μονάδα μετρήσει ὁ Η ἀριθμὸς ὤν"
• WRONG the Lean excerpt "is verbatim"
  research/proof-poem-seven-modes/lean/Euclid.lean:122 : the page dropped `have hp2 : 2 ≤ p := hp.1`; without it the excerpt fails (omega) and the footprint gains sorryAx
• WRONG note 4: the volta at "Yet what prime root?", lines 9-10 held, conclusion 11-14
  public/strata/proof-poem-seven-modes/index.html (the sonnet as printed) : no such line; the page's own gloss puts the turn at 9-11 and the conclusion at 12-14
• WRONG note 5, §V, §VIII: the case split "q ∈ S or q ∉ S" needs excluded middle; the proof is non-constructive, "does not identify q"
  https://en.wikipedia.org/wiki/Euclid%27s_theorem : membership in a finite set of naturals is decidable; the least factor is found by trial division; Euclid's is a direct proof by cases (Hardy and Woodgold 2009)
• WRONG note 7: Hardy §11, "a maker of patterns"
  https://archive.org/download/agt-mathsapology-hardy-9f4b21/mathsapology-hardy_djvu.txt : §10
• WRONG note 15: Hardy §18, "a far finer gambit"
  https://archive.org/download/agt-mathsapology-hardy-9f4b21/mathsapology-hardy_djvu.txt : §12
• WRONG notes 12 and 14: RFM I §155 ("MOTLEY"), I §26 ("changes the grammar")
  https://plato.stanford.edu/entries/wittgenstein-mathematics/ : RFM III §46 and III §31
• WRONG note 6: Formal and Transcendental Logic, trans. Dorothea Cairns
  https://philpapers.org/rec/HUSFAT-3 : Dorion Cairns
• CONFIRMED Heath Vol. 1 pp. 46-63 cover the textual tradition
  https://archive.org/details/bub_gb_UhgPAAAAIAAJ : chapter V, "The Text"
• CONFIRMED Heath's English of IX.20 (the page's "after Heath")
  https://archive.org/details/bub_gb_lxkPAAAAIAAJ : "Prime numbers are more than any assigned multitude of prime numbers"
• CONFIRMED Hardy epigraph on patterns
  https://archive.org/download/agt-mathsapology-hardy-9f4b21/mathsapology-hardy_djvu.txt : §10
• CONFIRMED Hardy §12, "as fresh and significant", Euclid one of two examples
  https://archive.org/download/agt-mathsapology-hardy-9f4b21/mathsapology-hardy_djvu.txt : §12
• CONFIRMED Hardy §18, "unexpectedness, combined with inevitability and economy"
  https://archive.org/download/agt-mathsapology-hardy-9f4b21/mathsapology-hardy_djvu.txt : §18
• CONFIRMED Hardy gives the complete-list version
  https://archive.org/download/agt-mathsapology-hardy-9f4b21/mathsapology-hardy_djvu.txt : "Let us suppose that it does, and that ... is the complete series"
• CONFIRMED de Moura and Ullrich, CADE-28 (2021) pp. 625-635
  https://doi.org/10.1007/978-3-030-79876-5_37 : matches
• CONFIRMED Barendregt and Wiedijk, Phil. Trans. R. Soc. A 363 (2005) 2351-2375
  https://doi.org/10.1098/rsta.2005.1650 : matches
• CONFIRMED Hales et al., Forum of Mathematics, Pi 5 (2017) e2
  https://doi.org/10.1017/fmp.2017.1 : matches
• CONFIRMED the Lean axiom transcript; no sorry, no Classical.choice, no native_decide
  /checks/research/proof-poem-seven-modes/lean/Euclid.lean : rerun, identical
• UNVERIFIABLE Lakatos's words "surveyable and criticizable" (note 11)
  search : not found; reads as paraphrase

What was done

• [fixed] Note 3: the nonexistent Gazette article and the misquoted Heath withdrawn, each named in the note; Heath's real sentence quoted, and the misremembering point credited to Hardy and Woodgold, "Prime Simplicity", Math. Intelligencer 31(4) (2009) 44-52, which exists and makes it.
• [fixed] §I and note 1: the 888 date and scribe belong to the Bodleian manuscript; Vatican 190 is the ante-Theonine witness Heiberg built on.
• [fixed] The Greek block replaced by Heiberg's text as Perseus encodes it, spacing tidied only; note 1 says so.
• [fixed] The Lean excerpt restored to verbatim (the hp2 line).
• [fixed] Note 4 rewritten for the sonnet as printed.
• [fixed] Constructivity: note 5, the §V proof-tree paragraph and the §VIII paragraph corrected; the eighth mode is now described as certifying a constructiveness Euclid's argument always had, not as rescuing it.
• [fixed] Hardy's section numbers: note 7 now §10, note 15 now §12.
• [fixed] Wittgenstein's: note 12 now RFM III §46, note 14 now RFM III §31.
• [fixed] Note 6's translator is Dorion Cairns. Also, outside the counted claims: Hadamard's note no longer says he surveyed Poincaré and Hermite (both dead decades before the inquiry), and the Lakatos phrase is marked as this page's paraphrase.
• [fixed] Reader check: the caption links the served Euclid.lean and says where to put it, and verify.mjs now skips with a fetch command, instead of failing, when Lean is present and the file is not.
• [fixed] A dated correction at the head of the notes lists everything above.
• [declined] The title says 7 ways and the dek 8: the slug and title predate the eighth mode; framing, not a factual claim.