Correctness, Artificial Intelligence, and the Epistemic Value of Mathematical Proof

TL;DR

This paper explores the nuanced relationship between correctness, epistemic value, and AI in mathematics, arguing that formal correctness is neither necessary nor sufficient for epistemic value and discussing implications for automated theorem proving.

Contribution

It offers a new perspective on the role of formal correctness in mathematical epistemology and its implications for AI and automated theorem proving.

Findings

Formal correctness is neither necessary nor sufficient for epistemic value.

Clarifies the relationship between mathematics, logic, and formal proof systems.

Discusses implications for AI applications in mathematics and automated theorem proving.

Abstract

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.