When Proofs Are Abundant, What Is a Paper For?

원문 초록

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.