It is kind of odd to ask for a credibility of a comment from someone who invented the field, but let me introduce one of Stephen Cook's comments supposing when the situation comes out as p=np.
"... it would transform mathematics by allowing a computer to find a formal proof of any theorem which has a proof of a reasonable length, since formal proofs can easily be recognized in polynomial time. Example problems may well include all of the CMI prize problems." [source]
I've always thought Gödel’s Incompleteness Theorems imply that an automatic machine which verifies the proof of every mathematical statement under any kind of consistent formal system is impossible.
Were my thoughts wrong? Or if I was not wrong, then what was Stephen Cook trying to say with his words?
I may guess, he was trying to insist that an automatic proof machine under some restricted conditions might be possible, only if when there is some effective solution to p=np.
Or there can be some another interpretation that he was premising 'verifying proof' and 'finding proof' are different in nature. However it arises a question that how can a machine 'find a proof' if it can't 'verify a proof'.
Could someone explain me the meaning of the comment from Stephen Cook? Thanks.
The key part of the quote that you're missing is "any theorem which has a proof of a reasonable length". Gödel's theorems imply that there are mathematical statements for which we can cannot prove or ¬. Cook's comment applies only to statements which do admit proofs, and moreover proofs "of a reasonable length".
Fix some polynomial $p$, and a polynomial time enumeration of mathematical statements, and consider the question $Q_p(n)$: "does statement $n$ admit a proof of length at most $p(n)$?" A "yes" answer to $Q_p(n)$ is witnessed by a proof of statement $n$ of length at most $p(n)$. Now there is a polynomial time algorithm to verify proofs of polynomially bounded length, so there is an NP algorithm to answer question $Q_p$. Thus if P=NP, there is a polynomial time algorithm to answer question $Q_p$, for any fixed polynomial $p$.
Note that a "no" answer to question $Q_p(n)$ tells us nothing. Maybe statement $n$ is provable, but the shortest proof is longer than $p(n)$. Or maybe statement $n$ is provably false, or even independent of ZFC. So the way we would use the algorithm is to guess a polynomial $p$, use as input a statement $n$ we're interested in, and hope that we get a "yes" answer: that statement $n$ has a proof of length at most $p(n)$. We could, in theory, use this method to settle open questions: there are mathematical statements (which we hope include the CMI prize problems!) which admit proofs of a reasonable length, but we haven't found these proofs yet.
However, it's not totally clear that such a method would transform mathematics, as Cook suggests. For one thing, the algorithm might give us a "yes" answer to $Q_p(n)$ without actually constructing a proof. The idea of accepting a computational answer promising that a proof of statement $n$ exists as a valid substitute for an "actual" proof of statement $n$ would no doubt be very controversial (see, e.g. the controversies around computer-assisted proofs of theorems like the four color theorem).
Secondly, as a practical matter, it's quite possible that the polynomial time algorithm solving problem $Q_p$ might run in time $O(x^N)$, where $N$ is much much much larger than the degree of $p$. The result of this might be that we could tractably detect whether statements admit very short proofs, but the algorithm is not actually feasible in practice for interesting inputs.