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

TL;DR

The paper argues that formal correctness is not the sole determiner of epistemic value in mathematics and that proofs gain value through their role in mathematical practice — definitions, methods, explanations, and the collaborative process of discovery. It advances an anti-logicist perspective, treating logic as a modeling framework rather than the ultimate foundation of mathematical truth. Through historical cases of fruitful errors (e.g., Poincaré, Frege), it shows that nonformalizable or even incorrect attempts can profoundly influence future mathematics. The discussion extends to AI and automated theorem proving, contending that AI can assist but cannot replace human-driven, socially situated mathematical inquiry, and that the value of proofs lies in the broader practice, not merely in formal derivations.

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.