I don't understand how this can be true given Godel's Incompleteness Theorem. The theorem shows that not all true statements in the second order Peano axiomati

I don't understand how this can be true given Godel's Incompleteness Theorem. The theorem shows that not all true statements in the second order Peano axiomatic system for the integers can be formally proven by a computer. That is, no first order axiomatic system for the integers is rich enough to capture all true statements in the second order system. The statement, '...allowing a computer to find a formal proof of any theorem which has a proof of reasonable length...' is where the problem lies. How does one determine which statements have proofs of reasonable length? I believe this is tied in with the Halting Problem. You just can't tell when something will be provable formally and when it can't. A proof of P=NP is not going to destroy mathematics.