If P=NP, could we obtain proofs of Goldbach's Conjecture etc.? 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!
Indeed!

If P=NP, not only we can decide whether there exists a proof of length n for Goldbach's Conjecture (or any other mathematical statement), but we can also find it efficiently!

Why? Because we can ask: is there a proof conditioned on the first bit being ..., then, is there a proof conditioned on the first two bits being ...., and so on...

And how would you know n? You'll just try all possibilities, in increasing order. When we make a step in the i'th possibility we also try a step in each of the possibilities 1..(i-1).