More directly, what I meant to say is that since there exist true theorems which cannot be proven within any particular choice of mathematical formalism, we need to operate with tools beyond simply symbolic manipulation. That was the death knell of Hilbert's Program and solidly separated the formal specification of math from "that thing which we're studying".
I'm not really sure that you mean about the "formal specification" for math vs. the "that thing we're studying". An informal (ie, not expressed in ZFC + 1rst order predicate calculus) proof of something non-trivial can go on for dozens, if not hundreds of dense pages of symbols. If I recall correctly, Whitehead's Principae Mathematica derived arithmetic from ZCF and predicate calculus, and it took the whole book.
I did a little reading to refresh myself on the subject, and this stood out as a good summary of the topic:
"In a sense, the crisis has not been resolved, but faded away: most mathematicians either do not work from axiomatic systems, or if they do, do not doubt the consistency of ZFC, generally their preferred axiomatic system. In most of mathematics as it is practiced, the various logical paradoxes never played a role anyway, and in those branches in which they do (such as logic and category theory), they may be avoided."
I mostly wanted to walk around the historical event I mentioned, the breaking of the Hilbert Program. At the time, it seemed that formal specification of math would provide a complete picture of what math was! Once the Program was finished then the job of mathematician would eke out into "computer" (of the abacus sort) or into other fields which interpreted the canon.
I'm not sure which death stroke was stronger, the incredible opaqueness and complexity of proof systems like ZFC or Gödel just saying what he was trying was outright impossible, but Hilbert's Program was killed before it even seriously took off, leaving the study of mathematics and the practical formalisms we use to study it pretty ad-hoc instead of grand and unified.
I'm unifying that with the fact that the way math seems to be practiced never comes from the formal language but instead first comes from imagining some kind of "mathematical object" and then taming its behavior with formalisms. You could consider them to be one and the same and argue that the difference is highly philosophical, and then this is where I'd invoke Gödel and inform you that there definitely exist things we could benefit from reasoning about that your formal language would fail to describe. This existence proof separates the classes of true things and provable things and makes their distinction more than philosophical.
Now, talking about what a "mathematical object" is gets you to the bleeding heart of the philosophy of science and epistemology. It's a tough question!
As a final note, ZFC is ZF + Axiom of Choice... which, yes, most practicing mathematicians just accept AoC so that they can integrate or whatever. The formal world without AoC is very sparse, but nobody has any sort of idea what the arbitrary decision means. I know that there has been some significant study of ZF-C, though it's been "impractical", I don't know if anyone is willing or capable of stating that ZF-C is in any way worse than ZFC. Impractical is a Mathematicians favorite adjective, so they're just two extant formal systems which disagree quite a lot on important things but we mostly pay attention to ZFC.