In $\mathbf{Q}$ (or any theory strong enough to encode $\mathbf{Q}$), there exist true statements whose proofs cannot be written in under $N$ symbols for a fixed $N$. For example, if $N = 1000000$ take the statement
This sentence has no proof with less than 1000000 symbols.
This can be formalized into the language of $\mathbf{Q}$ (or whatever sufficient strong theory we're using) and it has to be true, assuming consistency of our theory.
I'm interested in examples of natural-sounding statements such that we provably know that if the statement is true, then it's formal proof has an unreasonable lower bound on length. Since "unreasonable" is fairly subjective, lets say proofs that couldn't be written down over the lifespan of the entire universe if we could write a symbol a second.