Surely not? If there are more numbers that can be represented in any amount of bytes (as shown by the diagonal argument), then you cannot represent a constructive proof for each of them in any amount of bytes.
Kind of. A constructive proof by definition means something like you can explain exactly what the number is in a finite number of bytes.
The standard diagonalization argument is a constructive proof, identifying a specific number. Normally a constructive proof is preferable. But with a bit of hand waving you can make it into a non-constructive proof that there are "unknowable" numbers that cannot be described in any finite amount of bytes.
In practice constructible for reals mean that you can approximate them with arbitrarily small know precision e.g. a sequence of retional number numbers q_n each no more that 1/n apart from the actual real number.
The point is that such a sequence needs to be constructive in the usual sense, so there are still only a countable number of them.
The argument still applies, yes. Nevertheless the string still contains all finite substrings, which includes all English sentences describing such numbers.
The implication is that human minds wouldn't be able to represent it either, at least not with language.
