You’re smuggling in a frame here which isn’t obviously true: that mathematics is not just a collection of facts
It's a game of string transformations, where the goal is to produce specific strings given a set of rules.
The (syntactically valid) strings would correspond to statements, a producible string a theorem, and the production the proof.
I've done both of those things. I know what you get taught. But I've kept my math education going for the 25 years since then. I've talked to practicing mathematicians about what they do. I've learned a lot about the scope of math.
As an aside: most people really dislike it when I say that they should be much more precise about different numerical systems. The integers are not a subset of the rationals. They are entirely different constructions, but there is an isomorphism between integers and a subset of the rationals that preserves the integers' ring structure within that subset of the rationals and a few other aesthetic concerns. You can see why no one wants to communicate like this, even if they acknowledge it's technically correct. So I know all about pushing symbols around.
But I also know that pushing symbols around isn't the whole story. Pushing symbols around is only useful as a final check. Do you want to validate that 1+2=3? Pushing symbols around can help. But how do you decide that the ideas behind 1, 2, 3, +, and = are worth having precise and compact representations?
Math doesn't just use formal systems to generate proofs. It's not enough for symbols to be arranged neatly according to some rules. Math is also the process of creating the sets of symbols and their rules and communicating to other people why this set of rules and symbols is interesting. What ideas get preserved when you are working with this system? What is it an abstraction over?
This actually strikes me as a very formal perspective.
Considering it from an informal perspective, it's a bit more fuzzy isn't it. As you say there are many isomorphic things, and when we say The Integers it's not actually clear which one of them we mean. Maybe we mean one of them today and another tomorrow. Often times it doesn't matter, and so we don't clarify the question.
Like you could imagine defining the BootstrapNaturals then the BootstrapIntegers then the BootstrapRationals then use them to define the Reals. And then say that the Naturals, Integers and Rationals are defined as subsets of the Reals. This would be one way to put the common view of the Naturals as being a subset of the Reals on a solid formal foundation. It's rarely done ig because it's seen as obviously unproblematic to be a bit handwavy.
Another criticism of the common construction of numbers we could pose, inspired by object oriented programming, is that they fail at "information hiding". In programming an object should ideally not expose its internals. But in mathematics we may define 0 as say the empty set, making set operations on numbers syntactically valid which is kinda strange.
But yeah I think everyone has a sort of implicit understanding that 0 isn't actually the empty set. That it's merely a sort of hmm... thought experiment? That considering it 0 is a limited time offer, for the duration of the definition phase?
Maybe we come back to the isomorphism after all. "The natural numbers are something isomorphic to this set stuff I will now do"