Let $p(n)$ be the sentence $\neg Prf_{\text{PA}}(\underline n,\lceil 0=1\rceil)$, which means that the sentence $0=1$ can't be proved in Peano arithmetic with length $\leq n$.
Assuming $\text{Con}(\text{PA})$, $p(n)$ can be proved in $\text{PRA}$ with $O(n\cdot2^n)$ length, by enumerating all possible proofs with length $n$, and check them doesn't prove $0＝1$ one by one.
But is it the lowest bound? Are there one way to prove $p(n)$ in fewer length, such as $O(n)$？
Emil Jerabek's MO answer addresses this question quite thoroughly; I've very briefly summarized it here. I've made this CW to avoid reputation gain, and if Emil adds his own answer here I'll delete this one. Also, apologies to Emil of course if I got any of this wrong!
Let's start by replacing $\mathsf{PRA}$ with $\mathsf{PA}$, here - that is, we're looking at how difficult it is for $\mathsf{PA}$ to tell that $\mathsf{PA}$ has no contradictions of length $n$. At this point a metatheorem of Pudlak can be directly applied. The following is a quote from his 1984 paper On the lengths of finitistic consistency statements in first-order theories:
"The main results ... can be roughly stated as follows: Let $\mathsf{Con}_T(x)$ be a reasonable formalization of "there is no proof of contradiction in $T$ whose length is $\le x$." Then for reasonable $T$ there exist $\varepsilon>0$ and $k\in\omega$ such that
(1) any proof of $\mathsf{Con}_T(\underline{n})$ in $T$ has length $\ge n^\varepsilon$;
(2) there exists a proof of $\mathsf{Con}_T(\underline{n})$ in $T$ with length $\le n^k$."
(Re: attribution, Pudlak states in a footnote that the lower bound result was independently achieved by H. Friedman.) So there is a broadly-applicable metatheorem ... in exactly the opposite direction to what I expected!
But you ask about what the theory $\mathsf{PRA}$ proves about short contradictions in $\mathsf{PA}$ instead - in the language of the MO post linked above, you're asking about $p_\mathsf{PRA}$ instead of $p_\mathsf{PA}$ - and this is more complicated. In fact, even seemingly-"obvious" conjectures around this topic are wide open.
For more details, including sources, see Emil's above-linked answer.
