The Derivation-Indicator View of Mathematical Practice

This is the authors' abstract. We don't add key points for this paper.

A version of Formalism is vindicated: Ordinary mathematical proofs indicate (one or another) mechanically checkable derivation of theorems from the assumptions those ordinary mathematical proofs presuppose. The indicator view explains why mathematicians agree so readily on results established by proofs in ordinary language that are (palpably) not mechanically checkable. Mechanically checkable derivations in this way structure ordinary mathematical practice without its being the case that ordinary mathematical proofs can be ‘reduced to’ such derivations. In this way, one threat to formalist-style positions is removed: Platonic objects aren't needed to explain how mathematicians understand the import of ordinary mathematical proofs.