Unfortunately, constructive vs classical (vs linear, etc.) applies to proofs, but this is really about definitions. Proofs can be correct or incorrect pretty straightforwardly, but definitions being correct or not is really a matter of taste. (And as someone who's been formalising some mathematics in Lean recently, definitions are so much trickier to get right than proofs!)
My understanding is that since any mathematical proof can (in principle) be reduced to manipulation with formal objects (symbols), it’s always “constructive.”
Not really. Check out the proof of Hilbert's Nullstellensatz. He got tons of criticism for proving the existence of a relation without constructing that relation.
