This is not true, see Gödel's completeness theorem [1], which states "... that a deductive system of first-order predicate calculus is 'complete' in the sense that no additional inference rules are required to prove all the logically valid formulas." It basically means that every "true" statements are provable with a good enough deductive system.
What you possibly think about is Gödel's first incompleteness theorem [2] which is quite a different statement. It states that in "most" formal systems (that are complex enough to be able to describe natural numbers) there is always a statement A that both A and "not A" are not provable. It basically means that these statements can't be "logically valid", which means that there exist models of the formal system where A is true and models where "not A" is true.
[1] https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_th... [2] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
Basically, checking a proof for correctness takes polynomial time in the size of the proof. (Dependending on how you formalize your proofs, that might even be linear.)
Coming up with a reasonable sized proof is much harder. But if we had P=NP, then checking and finding a proof would be about equally hard.