Just because I say that objective mathematical truth exists, it doesn't mean that I think that formalism is unnecessary. On the contrary, formalism is the means by which we get at mathematical truth, so the limitations of formalism cannot be avoided. But regardless, our theorems "touch" things that exist independently of our choices of description.
It's like the difference between a description of the Rock of Gibraltar and the Rock itself. I can write about it in a hundred different languages, and some of the things I say in one language won't even make sense when translated into another. Now a formalist comes along and points out that the letters that I put onto paper are a shifting sand: many readings are possible even for a given statement, and not all are equivalent, despite my pains to make the descriptions as accurate as possible. Perhaps he even concludes on the basis of this that the Rock doesn't exist.
My answer is that the descriptions aren't the Rock itself. I can't get the Rock onto paper. But nevertheless the Rock has an objective existence that is independent of whatever I write about it, and the statements do refer to it. Insofar as the statements are correct in the context of their own languages, the statements reflect the properties of the Rock.
A formalist, however, goes to great pains to prove that 7 is prime using no more than his axiom set.
Fair enough, perhaps that was a bad example. Here's another: Gödel's theorem. It's different from the primality of seven, because it doesn't assume a formal system. It is a statement about all possible formal systems. It goes beyond formalism; it's true before I even pick an axiom set. Here's another (related) example: the universality of computation.
So who's the chick you two are trying to impress?
Godel's Theorem applies only to mathematical systems that encompass arithmetic of whole numbers. Other systems may be exempt. In fact, Godel himself demonstrated consistency of the predicate calculus.
The point is that a formalist would argue that Godel's Theorem devolves from the axioms used to derive it. It's true only because of the structure of the axiom set.
Hard-core intuitionists may not even regard it as an established proof because its proof requires that arithmetic be consistent, and if it's true then the Theorem itself implies that arithmetic cannot be shown to be consistent through the underlying axiom set. That is, Godel's Theorem is provable only if you can prove something that Godel's Theorem shows to be unprovable.