It has been argued that an appropriate version of Gödel's first incompleteness theorem shows the following: our naive system of mathematical proof is recursively enumerable (re) iff it is inconsistent (*). \textit{J. Lucas} [``Minds, machines and Gödel'', Philosophy 36, 112- 127 (1961), and elsewhere] argued that the system is consistent, and inferred that the mind is not a computer; the reviewer [J. Philos. Log. 13, 153-179 (1984; Zbl 0543.03004), and elsewhere] argued that proof is re and inferred that it is inconsistent. This paper takes issue with (*), and hence with the arguments of Lucas and the reviewer. The central point is that the argument for (*) trades on an ambiguity between two notions of proof: one is the familiar one; the other is called `R-proof'. A statement is R-provable in system \(S\) iff it is provable as a system that can be represented (in a certain sense) in \(S\). In the reviewer's opinion, the argument does not trade on this ambiguity, but works for the simple notion of proof. See the reviewer, ``Yu and your mind'', Synthese (to appear).