arXivDaily arXiv每日学术速递 周一至周五更新
arXiv周末暂无论文更新,休息一下吧,周末愉快~~

审计下的计算机辅助证明:符号可逆性证明中的排版错误、证书错误及可复现的精确检查

Computer-assisted Proof Under Audit: Typos, Certificate Errors, and Reproducible Exact Checks for a Symbolic Invertibility Proof

Fan Zheng

arXiv 2608.13067首次发表:更新:

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

论文原文

arXiv 摘要页 · PDF 原文 · HTML 原文

↑