Theorems that won't be proved by a computer

Question

I want to prove in the following way there is a statement that a computer can't prove. Suppose the time of life of our universe is limited by $t$ and the speed of calculations is limited by $s$. Now, consider the axioms of Peano arithmetic (PA). Can we show that for a given $n$ (in particular, $n=ts$), there is a sentence $S(n)$ provable in PA, such that the minimal number of strings in a (Hilbert-style) proof of $S(n)$ is greater than $n$?