Most real numbers have infinite-length constructive proofs.
Uncountable is uncountable is uncountable. If any correspondence/encoding existed between naturals and reals, the reals would be countable. (But they are not, so it is fool's errand to search for such an encoding.)
The implication is that human minds wouldn't be able to represent it either, at least not with language.
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.
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.
But it couldn't contain the real number representation.