Comment by skew-aberration

That's not that how that works btw. The incompleteness is a property of the algorithm which does the proofs, not the theorems. If a theorem is true it has a proof and a program which proves it (printf("the proof verbatim")). But no computer program can successfully prove all theorems. The space of potential proofs is too big to search systematically, but you can still get lucky.