arXiv cs.AI· Charles-Albert Lehalle·· 10 小时前AI 评分34
当证明变得唾手可得，论文还有什么用？
When Proofs Are Abundant, What Is a Paper For?
AI 导读
面对 AI 系统不断产出形式化验证的证明、正确证明的成本趋近于零，有研究提出论文的价值不止于一个被验证的陈述，还在于作者的问题选择与视角（Derivation-Level Intension）以及从结果到论证的推理链条（Directional Extension）。
正文 · AI 翻译
摘要：AI 系统如今能为著名的未解问题生成经过形式化验证的证明，而获得正确证明的成本正趋近于零。如果正确性变得廉价，那么研究论文还剩下什么需要传达？我认为，一篇论文并不能被一个经过验证的陈述所穷尽。它是一个暴露于共同体批评之下的叙事，由一种内涵（作者对问题与视角的选择）、一条科学思维链（通向结果的推理步骤）以及支撑每一步的论证构成。已发表的大多数数学成果是依据这两个要素而非仅凭正确性来评判的，而机器生成的形式化脚本两者都无法传达。借用逻辑学与类型论，我将前者形式化为“推导层内涵”，将后者形式化为“有向延拓”：把证明分解为若干割点，其公理足迹揭示出它的薄弱环节（结果可在何处得到加强）与强健环节（可迁移至其他理论）。此外，我考察了 AI 在研究过程中可扮演的五种角色，包括文献检索与批判性判断，并表明它们中没有一个能免除声明这两个要素的必要性。我提及了这两个概念对期刊以及对 AI 时代年轻数学家培养可能有所助益的方式。如果证明变得充裕，稀缺资源便不是正确性，而是共同体对某个结果为何重要、如何能进一步推进的共识理解。
| 主题： | 计算机科学中的逻辑（cs.LO）；人工智能（cs.AI） |
| 引用为： | arXiv:2611.12943 [cs.LO] |
| （或 arXiv:2611.12943v1 [cs.LO] 为本版本） | |
| https://doi.org/10.48550/arXiv.2611.12943 由 DataCite 颁发 arXiv DOI |
提交历史
来自：Charles-Albert Lehalle [查看邮箱] [经由 CCSD 代理]
[v1]
2026年11月6日星期五 17:38:16 UTC（25 KB）
来源：arXiv cs.AI · arxiv.org