  We prove that any proof of a $\forall \Sigma^0_2$ sentence in the theory
$\mathrm{WKL}_0 + \mathrm{RT}^2_2$ can be translated into a proof in
$\mathrm{RCA}_0$ at the cost of a polynomial increase in size. In fact, the
proof in $\mathrm{RCA}_0$ can be found by a polynomial-time algorithm. On the
other hand, $\mathrm{RT}^2_2$ has non-elementary speedup over the weaker base
theory $\mathrm{RCA}^*_0$ for proofs of $\Sigma_1$ sentences.
  We also show that for $n \ge 0$, proofs of $\Pi_{n+2}$ sentences in
$\mathrm{B}\Sigma_{n+1}+\exp$ can be translated into proofs in
$\mathrm{I}\Sigma_{n} + \exp$ at polynomial cost. Moreover, the
$\Pi_{n+2}$-conservativity of $\mathrm{B}\Sigma_{n+1} + \exp$ over
$\mathrm{I}\Sigma_{n} + \exp$ can be proved in $\mathrm{PV}$, a fragment of
bounded arithmetic corresponding to polynomial-time computation. For $n \ge 1$,
this answers a question of Clote, H\'ajek, and Paris.
