Every conjecture that is provable can be proved by the proposed program of length (conjecture + constant) in finite time. That was the original statement: > y

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.