Computer-assisted Proof Under Audit: Typos, Certificate Errors, and Reproducible Exact Checks for a Symbolic Invertibility Proof
arXiv:2608.13067
Abstract
We audit the exact-arithmetic certificate in arXiv:2310.19781v2, its 2025 \emph{Communications in Mathematical Physics} version, and their shared MATLAB archive. CMP corrects none of the audited items; we therefore treat both versions together and use the openly accessible arXiv source for exact provenance. We found 11 proof-affecting defects (alongside typographical slips) and give reproducible exact counterexamples to several implemented bounds and reconstruction steps. To the best of our knowledge, this is the first independent, version-pinned, source-level audit of a published computer-assisted proof (CAP) in analysis to identify multiple proof-affecting defects in its released computational certificate. The findings do not refute the intended theorem or its analytic reduction, but they show that the published certificate does not prove the claimed conclusion. Future work will give a corrected, structurally simpler proof with substantially less machine assistance.
28 pages, no figure