On the unreasonable reliability of mathematical inference

Abstract

In (Avigad, 2020), Jeremy Avigad makes a novel and insightful argument, which he presents as part of a defence of the ‘Standard View’ about the relationship between informal mathematical proofs (that is, the proofs that mathematicians write for each other and publish in mathematics journals, which may in spite of their ‘informal’ label be rather more formal than other kinds of scientific communication) and their corresponding formal derivations (‘formal’ in the sense of computer science and mathematical logic). His argument considers the various strategies by means of which mathematicians can write informal proofs that meet mathematical standards of rigour, in spite of the prodigious length, complexity and conceptual difficulty that some proofs exhibit. He takes it that showing that and how such strategies work is a necessary part of any defence of the Standard View. In this paper, I argue for two claims. The first is that Avigad’s list of strategies is no threat to critics of the Standard View. On the contrary, this observational core of heuristic advice in Avigad’s paper is agnostic between rival accounts of mathematical correctness. The second is that that Avigad’s project of accounting for the relation between formal and informal proofs requires an answer to a prior question: what sort of thing is an informal proof? His paper havers between two answers. One is that informal proofs are ultimately syntactic items that differ from formal derivations only in completeness and use of abbreviations. The other is that informal proofs are not purely syntactic items, and therefore the translation of an informal proof into a derivation is not a routine procedure but rather a creative act. Since the ‘syntactic’ reading of informal proofs reduces the Standard View to triviality, makes a mystery of the valuable observational core of his paper, and underestimates the value of the achievements of mathematical logic, he should choose some version of the second option.