 First, whereas the collection of sentences provable in a formal system is always computably enumerable, we know much less about the extension of the concept of informal provability. Lucas (Lucas 1961), and later Penrose (Penrose 1989, 1994), have argued that informal mathematical provability outstrips provability in any given formal system. But their arguments are widely regarded as unpersuasive. Benacerraf has argued against Lucas and Penrose that it cannot be excluded that there is a formal system \(T\) such that in fact mathematical provability extensionally coincides with provability in \(T\), even though we cannot know that it does (Benacerraf 1967). Others have argued that the concept of informal mathematical provability is not even clear enough for the question whether its extension is computably enumerable to have a definite answer (Horsten &amp; Welch 2016).