Hard Proofs and Good Reasons

TL;DR

This paper explores the philosophical and computational challenges of understanding what constitutes good reasons for mathematical truths, questioning the reliance on proofs and proposing new perspectives on mathematical justification.

Contribution

It introduces a philosophical framework addressing the disconnect between mathematical truths and their proofs, considering implications for non-human mathematical reasoning.

Findings

Mathematicians may focus on reasonable truths without full proofs.

Many theorems have exponentially-long proofs, questioning their practical use.

New perspectives are needed to understand mathematical justification beyond proofs.

Abstract

Practicing mathematicians often assume that mathematical claims, when they are true, have good reasons to be true. Such a state of affairs is "unreasonable", in Wigner's sense, because basic results in computational complexity suggest that there are a large number of theorems that have only exponentially-long proofs, and such proofs can not serve as good reasons for the truths of what they establish. Either mathematicians are adept at encountering only the reasonable truths, or what mathematicians take to be good reasons do not always lead to equivalently good proofs. Both resolutions raise new problems: either, how it is that we come to care about the reasonable truths before we have any inkling of how they might be proved, or why there should be good reasons, beyond those of deductive proof, for the truth of mathematical statements. Taking this dilemma seriously provides a new way to make sense of the unstable ontologies found in contemporary mathematics, and new ways to understand how non-human, but intelligent, systems might found new mathematics on inhuman "alien" lemmas.