 We know much about the concepts of formal proof and formal provability, their connection with algorithmic computability, and the principles by which these concepts are governed. We know, for instance, that the proofs of a formal system are computably enumerable, and that provability in a sound (strong enough) formal system is subject to Gödel’s incompleteness theorems. But a mathematical proof as you find it in a mathematical journal is not a formal proof in the sense of the logicians: it is a (rigorous) informal proof (Myhill 1960, Detlefsen 1992, Antonutti 2010).