数学证明的真理性不依赖形式正确性，人工智能时代更需重新思考证明的本质。
Correctness, Artificial Intelligence, and the Epistemic Value of Mathematical Proof
- 证明的真理价值不取决于能否形式化
- 形式正确性只是数学证明的辅助条件
- 为AI辅助数学提供哲学基础，适合逻辑与数学哲学研究者
我们认为，数学证明具有认识论价值，并不要求其在形式证明系统中可形式化。我们提出一种数学与逻辑关系的新观点，阐明形式正确性在数学中的作用。最后，讨论这些论点对自动化定理证明及人工智能在数学中应用的相关争论的意义。
原文摘要 · Abstract (English)
We argue that it is neither necessary nor sufficient for a mathematical proof to have epistemic value that it be "correct", in the sense of formalizable in a formal proof system. We then present a view on the relationship between mathematics and logic that clarifies the role of formal correctness in mathematics. Finally, we discuss the significance of these arguments for recent discussions about automated theorem provers and applications of AI to mathematics.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。