This is a naive question, out of my expertise; apologies in advance.
Goldbach's Conjecture and many other unsolved questions in mathematics can be written as short formulas in predicate calculus. For example, Cook's paper "Can Computers Routinely Discover Mathematical Proofs?" formulates that conjecture as
$$\forall n [( n > 2 \wedge 2 | n) \supset \exists r \exists s (P(r) \wedge P(s) \wedge n = r + s) ]$$
If we restrict attention to polynomially-long proofs, then theorems with such proofs are in NP. So if P=NP, we could determine whether e.g. Goldbach's Conjecture is true in polynomial time.
My question is: Would we also be able to exhibit a proof in polynomial time?
Edit. As per the comments of Peter Shor and Kaveh, I should have qualified my claim that we could determine if Goldbach's conjecture is true if it indeed is one of the theorems with a short proof. Which of course we do not know!