Every conjecture that is provable can be proved by the proposed program of length (conjecture + constant) in finite time.

That was the original statement:

> you can encode any proof to a few hundred lines.

This type of encoding is funny of course. You can not determine from the encoding of the proof whether the encoding is the encoding of a proof (as you point out). But if you have a proof, and thus know that a proof exists you can "encode" it very succinctly in this program for whatever that is worth.