A correspondence problem for mathematical proof

TL;DR

This paper explores the concept of correspondence between formal derivations and mathematical proofs, emphasizing the importance of adequate representation and tracking, and discusses implications for the future of mathematical formalization.

Contribution

It introduces a nuanced account of what it means for a formal derivation to correspond to a proof, highlighting criteria beyond mere existence of formalizations.

Findings

Formalization systems vary in establishing correspondence criteria

Adequate representation and tracking are essential for meaningful formal proofs

Future mathematical formalization may face new challenges based on these criteria

Abstract

Mathematical proofs are often said to justify their conclusions by indicating the existence of a corresponding formal derivation. We argue that this widespread view relies on an under-examined notion of correspondence, or what it means for a particular derivation to ''correspond'' to a particular proof. Mere existence of a formalization is not enough, and a substantive account of the required correspondence resolves into two criteria -- adequate representation (of the original theorem) and tracking (of the steps in the original proof). An examination of the actually-existing formalization systems we have today shows the variety of quasi-empirical ways we establish these criteria, and points towards new burdens that may be placed on the future evolution of mathematics itself.