from wikipedia: "an expression like 'the smallest positive integer not definable in fewer than twelve words' (note that this defining phrase has fewer than twelve words)"
I thought of that too. Which leads me to think that the proof status of the OP's "theorem" is less clear. You cannot exhibit a deterministic algorithm that maps every English phrase to the integer that phrase describes, unless you are prepared to accept that some phrases like "the smallest positive integer not definable in fewer than twelve words", are meaningless or illegal. (The thing is, once you exhibit such a mapping, that phrase immediately obtains an obvious meaning, and so it "should" be included in the domain, which would then lead to a contradiction... so you will be stuck with an obviously deficient mapping.)
In that case, I'm not sure if you could write a formally rigorous proof in English. You might come up with some rule to monster-bar such meta-descriptive phrases as "the smallest positive integer not definable ..."; I suspect many such rules, perhaps all of them, would rule out the meta-descriptive language needed to state the conclusion. (How do you formally define "describable" without exhibiting an algorithm that computes integers from their descriptions? Perhaps you'd be satisfied by merely constraining what "describable" could mean...) Even if there are a few such rules under which the proof is valid English, is it not kind of arbitrary which rule you choose, and kind of empty to say "I proclaim this choice to be the right one, and then my proof is valid"?
from wikipedia: "an expression like 'the smallest positive integer not definable in fewer than twelve words' (note that this defining phrase has fewer than twelve words)"