Right. Of course, the point of the theorem is to show by analogy that DNA could have arisen by chance. That discussion involves Dawkins versus creative design, and involves biology as well as statistical probability. Probably a different forum!
It doesn't have to be written down yet. But since the conjecture hasn't been proven yet we can't be sure if it's true or not. If the conjecture isn't true then we can't write down a proof of the theorem itself (and have it be correct). And due to the Incompleteness theorem it theoretically might not even be possible to write down a proof even if it is true. A disproof would just need to show a counter-example so there would be no issues writing that down. Basically all I was saying was "assuming it's possible to write down that proof - then yes it will be written almost surely".
I still think that because it's possible that any given string of characters might NOT be produced randomly during infinity it can't be statistically right to say that it will be. And I still think that the original questioner had a point about randomness not being able to produce language. That involves the philosophy of meaning. Another different forum. Thanks for taking me seriously. I'll leave you all to your maths!