Title: Informal Proofs and Formalisation

Abstract: In this talk I will consider the problems posed by the "informal" proofs of actual mathematical practice. I shall focus on the family of views which aim to account for informal proofs in terms of underlying formal proofs (such as Jody Azzouni's derivation-indicator view), discussing desiderata that such theories are aiming to satisfy. I will argue that the kind of formalisation invoked by these accounts gives rise to a problem of associating informal proofs with too many different formal proofs, undermining the ways in which the accounts were hoping to satisfy the desiderata. Next, I argue that the success of formalisation projects, surprisingly, also do not provide support for such accounts. I will conclude that the formalisability of informal proofs is a red herring and that an alternative account is needed.