Trust, but Replay: Auditing Published Mathematical Claims

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 25 locked gates (17 BREAK / 8 PASS) fall into three strata with very different evidentiary weight: four historical calibrations, twelve 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 an unfinished formalization line; 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. TL;DRs for different audiences For the SME. A methods paper on fail-closed replay of published mathematical claims: 25 locked gates over six days (17 BREAK / 8 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 25 published claims and re-ran them from scratch, assuming each was wrong until the evidence said otherwise. Eight 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: 8 of 25 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 hand-re-executed all 25 gates and read every script and disposition before publication, 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. Six days, one investigator with AI tooling, 25 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. Six calendar days, one principal investigator plus AI agents, ~$0 marginal compute cost: 25 published claims independently replayed and dispositioned, a reusable audit playbook, a public repository, and a 12,000-word 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 (order-7 recurrence certificate, machine-checked). 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.