Trust, but Replay: Auditing Published Mathematical Claims

Bilar, Daniyel Yaacov · 2026-10-06 · v1.0.4 · publication/preprint · cc-by-4.0

Abstract

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), 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. Companion repository: github.com/chokmah-me/fragile-proof-audit. Gates refute routes, not theorems.

Keywords

proof audit · reproducibility · mathematical claims · computer-assisted proof · fail-closed replay · formal verification · research integrity · Lean 4

← All research