AI 中文总结
本研究对已发表的分析领域计算机辅助证明的证书开展源级审计,发现11处影响证明的缺陷及排版错误,给出反例,指出证书未证明结论,未来将提供更简单的修正证明。
AI 中文摘要
我们对arXiv:2310.19781v2中的精确算术证书、其2025年《数学物理通讯》(Communications in Mathematical Physics, CMP)版本以及二者共享的MATLAB归档文件进行了审计。CMP未修正任何经审计的项目;因此我们将两个版本一并处理,并使用公开可访问的arXiv源获取精确溯源信息。我们发现了11处影响证明的缺陷(连同排版错误),并针对若干已实现的界和重构步骤给出了可复现的精确反例。据我们所知,这是首次对已发表的分析领域计算机辅助证明(Computer-assisted proof, CAP)开展的独立、版本固定的源级审计,旨在识别其发布的计算证书中多处影响证明的缺陷。这些发现并未否定预期定理及其解析归约,但表明发布的证书并未证明所声称的结论。未来工作将提供修正后的、结构更简单的证明,所需机器辅助也将大幅减少。
英文摘要
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.
Comments28 pages, no figure