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）。
正文 · 原文
Abstract:AI systems now produce formally verified proofs of celebrated open problems, and the cost of obtaining a correct proof is falling toward zero. If correctness becomes cheap, what is left for a research paper to communicate? I argue that a paper is not exhausted by a verified statement. It is a narrative exposed to the criticism of a community, made of an intension (the author's choice of problem and perspective), a scientific chain of thought (the reasoning steps leading to the result), and the arguments supporting each step. Most published mathematics is judged on these two elements rather than on correctness alone, and machine-generated formal scripts convey neither. Borrowing from logic and type theory, I formalise the first as a Derivation-Level Intension and the second as a Directional Extension: a decomposition of a proof into cut-points whose axiomatic footprints reveal its weak links, where the result could be strengthened, and its strong links, which can be transported to other theories. Moreover, I examine five roles AI can play in the research process, including bibliographical search and critical judgment, and show that none of them removes the need to declare these two elements. I mention ways these two concepts could be useful for Journals and for training of young mathematicians in a AI era. If proofs become abundant, the scarce resource is not correctness but a community's shared understanding of why a result matters and how it could be pushed further.
| Subjects: | Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2611.12943 [cs.LO] |
| (or arXiv:2611.12943v1 [cs.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2611.12943 arXiv-issued DOI via DataCite |
Submission history
From: Charles-Albert Lehalle [view email] [via CCSD proxy]
[v1]
Fri, 6 Nov 2026 17:38:16 UTC (25 KB)
来源：arXiv cs.AI · arxiv.org