Gödel's speed up theorem and Matiyasevich polynomials Unless I am sadly mistaken, there should exist a polynomial  $ P\in\mathbb Z[X_1,X_2,\dots, X_n]$ coding for the speed-up theorem (for, say, ZFC), i.e. having the following properties : 
1) P has an integer root (i.e. $\exists (k_1,\dots,k_n)\in\mathbb N^n, P(k_1,\dots,k_n)=0$) 
2) P is explicit (i.e. n , the number of monomials of P, and the coefficients are all small (say $<10^4$).
3) The smallest proof of 1) in ZFC has more than $10^{10^{100}}$ symbols but
4) There exists a short (not much longer than P itself) proof of 1) in ZFC + Consis (ZFC)
a) Am I right ? b) is it obvious then that one of the $k_i$ is greater than $10^{10^{99}}$ ? c) and that all of the  $k_i$ (of the smallest solution) are computable ?
 A: I think you're right. 
In Gödel's speed-up theorem, one may consider the
statement $\sigma$, asserting that "there is no proof of $\sigma$
in PA of length less than a googolplex symbols." Now, if there
were a short proof of $\sigma$, in less than a googolplex symbols,
then we would be able to prove that the proof had that property,
and thereby prove a contradiction in PA. So if PA is consistent,
then $\sigma$ is true. Meanwhile, assuming again that PA is
consistent, then we can also see that $\sigma$ is actually provable in
PA, by enumerating all the proofs. So we see that in fact PA proves $\sigma$, but only
by a very long proof, whereas PA+Con(PA) provides a very quick proof of $\sigma$
by formalizing the argument we have just given.
Now, by the MRDP theorem, there is an integer polynomial $p(x,\vec
x)$ such that $p(k,\vec k)=0$ for integers just in case $k$ codes
a proof of $\sigma$ in PA. Although the coding of c.e. sets into
diophantine equations is complicated, it is ultimately managable,
and one can get an explicit polynomial $p$. I haven't worked out the polynomial explicitly — and I don't intend to do so — but I believe that the particular
bounds that
you mention are not unreasonable. It may be useful to compare with this polynomial, whose solutions are exactly the primes. The
difficulty of the primeness representation seems basically comparable to
yours, and this is why I think your bounds are reasonable.
So what we have is a comparatively small polynomial $p(x,\vec x)$,
such that PA proves that $\exists k,\vec k\ p(k,\vec k)=0$ and
furthermore proves that any such $k$ will be the code of a proof
of $\sigma$ in PA. Thus, there can be no short proof of this. But
meanwhile, PA+Con(PA) proves $\exists k,\vec k\ p(k,\vec k)=0$ by
a very short proof, which simply formalizes our argument above. So
we've got all your desired properties.
So I think (a) you're basically right; (b) yes, the $k$'s must be
large, for otherwise we could have a short proof of $\sigma$ just
by evaluating $p(k,\vec k)=0$, combined with the fact that PA
proves (by a short proof) that any such $k$ must code a proof of
$\sigma$. Regarding statement (c), however, I don't think it makes
any sense, because every particular natural number is computable,
by the algorithm that simply writes it down. If it was merely bounds on $k$ that you wanted, these are provided by the size of the proof of $\sigma$ in PA, which proceeds by enumerating all proofs of size less than a googolplex symbols, and noting that it is not a proof of $\sigma$. 
