Correctness, Artificial Intelligence, and the Epistemic Value of Mathematical Proof
This work addresses foundational issues in the philosophy of mathematics and AI, potentially influencing how AI tools are designed and evaluated for mathematical tasks.
The paper argues that formal correctness is neither necessary nor sufficient for a mathematical proof to have epistemic value, and it explores implications for AI applications in mathematics, such as automated theorem provers.
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.