Published mathematics is trusted far more than it is independently replayed. Peer review checks reasoning, not computation - and increasingly, part of the proof is a computation. This paper describes a short, intensive audit campaign (six calendar days, 2026-09-18 through 2026-09-23) that replays published mathematical claims from scratch under a hostile prior: every locked gate is built to produce the opposite verdict where the opposite is correct (the four exact-equality gates are exempt - Sec. 4.2), and a CI-enforced verdict lock fails loudly on drift in either direction. The contribution is the playbook, not the verdicts: a five-disposition taxonomy (BREAK, GAP, PASS, SKIP, UNKNOWN) with a polarity rule separating gate verdicts from claim-level dispositions; seven attack types classified by mechanism, each with a worked example; and the evidentiary disciplines - paper-first gating, discrimination controls, gate-before-prove, fail-closed replay, independent anchors - together with the record of where those disciplines were violated and what caught the violations. The 32 locked gates (17 BREAK / 15 PASS) fall into three strata with very different evidentiary weight: four historical calibrations, nineteen live-literature targets, and eight low-stakes preprints, plus one infrastructure oracle. Case studies include a refutation replay, an execution-verified confirmation, a canonization, and a correct-proof infrastructure line (q-TSPP); the limitations section states what no discipline closes. The campaign repository is public at https://github.com/chokmah-me/fragile-proof-audit. Gates refute routes, not theorems. ---------------------------This version (v1.0.4, 2026-10-06). Verdict lock grown 25 to 32 gates (17 BREAK / 15 PASS): the seven 2026-09-24 PASS audits pinned - five live-literature confirmations (Holden's C7 factorization, Holden's GMRES counterexample, Webb's d7 = 47, Maierhofer's pseudospectra, Heidary's Latala-Swiatkowski) plus the two-route Euler-blowup audit with a clean 32/32 re-run; repository-public line corrected; section 7 related-work entry on autoformalization (upstream, not overlapping); section 8 conclusion PASS count corrected (three to ten). Prefer concept DOI 10.5281/zenodo.22926995 for always-latest PDF. v1.0.3 (10.5281/zenodo.23148836) remains the prior PDF revision.---------------------------- TL;DRs for different audiences For the SME.A methods paper on fail-closed replay of published mathematical claims: 32 locked gates (17 BREAK / 15 PASS), stratified into historical calibrations, live-literature targets, and low-stakes preprints, plus one infrastructure oracle. The contribution is the playbook - five dispositions (BREAK, GAP, PASS, SKIP, UNKNOWN) with a polarity rule separating gate verdicts from claim-level dispositions, seven attack types classified by mechanism with a worked example each, and the evidentiary disciplines: paper-first gating, discrimination controls, gate-before-prove, hash-pinned inputs, independent anchors, and a CI-enforced verdict lock that fails loudly on drift in either direction. Limitations and control violations are documented, not buried. Repo public, SHA-pinned, archived at DOI 10.5281/zenodo.22926995. For the interested layman.Peer review checks the reasoning in a math paper, but increasingly part of the proof is a giant computer calculation nobody re-runs. This project took 32 published claims and re-ran them from scratch, assuming each was wrong until the evidence said otherwise. Fifteen claims survived; seventeen didn't - bad numbers, broken steps, gaps the reviewers missed. The point isn't that mathematics is broken, it's that "published" and "checked" aren't the same thing for computer-assisted proofs, and independent re-running should be a normal part of science. Everything's public so anyone can check the checking. For the skeptic.Yes, it finds breaks. It was also built to confirm: 15 of 32 gates PASSed, gates are calibrated against historical canons, and the verdict lock fails on drift in either direction, so a silently passing broken claim or a silently failing sound one both scream. The author directed a clean re-run of all 32 locked gates (32/32 ok, zero drift) and read every script and disposition before this draft, and the paper's limitations section states what no discipline closes - including that a gate verdict is about the route, not the theorem. All inputs are hash-pinned, all code public, all verdicts reproducible. If you don't trust it, re-run it; that's the entire point. For the decision maker.The gap is structural: journals certify proofs whose computational components are never independently executed. This paper delivers a concrete, cheap, adoptable answer - a gate-and-lock audit discipline that any journal, institute, or funding body could require for computational claims: independent replay under a hostile prior, discrimination controls, pinned inputs, a verdict lock that detects drift. One investigator with AI tooling, 32 claims adjudicated to a stable, versioned record. The infrastructure is public and archivable. If you fund or publish computational mathematics, this is the missing quality layer. For the funder.One principal investigator plus AI agents, ~$0 marginal compute cost: 32 published claims independently replayed and dispositioned, a reusable audit playbook, a public repository, and a methods paper with a Zenodo DOI. The next tranche scales it: a larger claim harvest, a standing CI-run verdict lock on the public repo, and the open q-TSPP formalization line in Lean 4. Deliverables are binary and verifiable: gates closed, verdicts locked, paper archived. You're buying the only known quality-control layer for an entire class of published mathematics.
proof audit · reproducibility · mathematical claims · computer-assisted proof · fail-closed replay · de Bruijn-Newman constant · formal verification · research integrity · computational mathematics · audit methodology · conjecture refutation · Lean 4