A Problem with the Dependence of Informal Proofs on Formal Proofs

In this paper I examine the phenomenon of informal proofs as found in mathematical practice and the difficulties these face concerning rigour and correctness.I focus on one particular type of response, which I call derivationist, which seeks to explain these in terms of underlying formal derivations.I proceed to set out five desiderata that the derivationist approach should aim to satisfy.With particular emphasis on Azzouni's derivation-indicator account, I raise a dilemma for the type of link that must be posited from informal proofs to formal derivations: that it must either be agent-independent or else agent-dependent.I show that derivationist theories want to take the first horn, but that considerations of proof identity, uniqueness and informal content determining formal structure are serious obstacles in that direction.I further argue that the other horn is incompatible with the original motivations of the derivationists.Thus I conclude that the desiderata for a derivationist theory cannot be satisfied.