An interesting and still valid point, however, is that P=NP may be undecidable (in the sense of Gödel's incompleteness theorem). In other words, our current axioms may be insufficient to prove or disprove P=NP.
http://www.scottaaronson.com/papers/pnp.pdf
> P != NP is either true or false. It’s one or the other. But we may not be able to prove which way it goes, and we may not be able to prove that we can’t prove it.
THEOREMS (the language of correct proofs) is in P; given a correct proof (possibly restricted to being in first-order logic), it can be verified in polynomial time. In the first-order logic case, all you have to do is read the proof from beginning to end and verify that each statement follows from either an axiom or an already-established statement. This is done entirely syntactically, requiring no knowledge of the underlying mathematics.
However, to do this requires formalizing the entire proof in machine-checkable format, which is a substantial undertaking even for relatively simple proofs and will likely take far longer than polynomial time.