it is easy to construct a formal system with which we have precisely that experience.

I included the qualification "the formal systems that you're thinking of". Were you thinking of that formal system when you wrote

There's a particular set of formal steps I can go through to convince myself that two numbers are twin primes, and a different set of steps which will convince me that some particular pair is the largest such pair, or that there isn't a largest pair.

?

By what standard are we to judge between formal systems in which 2 is provable, those in which it is disprovable, and those in which it cannot be proved either way? Do we take a vote? Is it a question of appeal to human intuition?

This is a separate question from your original one. To answer your original question, the platonist need only point to a particular formal system (e.g., PA), and say that the nonexistence of the number 2 would mean [ETA: rather, would imply] that there would be no proof of 2's existence in that particular system.

But the platonist would also find your new question interesting. For example, when you wrote "There's a particular set of formal steps ...", how did you come to settle on that particular set of formal steps?

One position would maintain that some particular formal system is implicit in the statement of the twin prime conjecture (TPC). That is, when someone asks "Are there infinitely many twin primes?", they are speaking in an abbreviated fashion, and they really mean "Does PA prove that there infinitely many twin primes?", or "Does ZFC prove that ...", or something like that. This position would claim that number-talk has meaning only when the speaker has some specific formal system in mind.

The difficulty with this position is that people seemed to be making meaningful assertions about numbers for thousands of years before settling on any formal systems of arithmetic — indeed before they even had the concept of a formal system. (Euclid's is presumably too unrigorous to count.) Ancient number-theory texts such as the Introduction to Arithmetic by Nicomachus often didn't even include anything like what we would call a proof, not even in the sense in which Euclid's arguments are called proofs. Nicomachus pretty much just flatly asserts number-theoretic propositions, perhaps bolstering his claims with a few examples. Yet somehow readers would reflect on these propositions and agree with them, even though Nicomachus didn't communicate which formal system he was working within.

Another position would maintain that people absorb some formal system implicitly from their culture, and their number-talk is automatically in terms of that formal system. Even if that culture lacks the concept of a formal system, nonetheless all its number-talk is governed by some formal system.

But it is not even known whether the TPC is decidable in any of the standard formal systems. Suppose that the TPC were proved undecidable in, say, ZFC. Would the question really then lose all meaning? Consider a physical computer that brute-force factors one odd number after the next, and prints every consecutive pair of odd numbers that have no nontrivial factorizations. Would it really become meaningless to ask whether there is a bound on how many entries the computer would print, regardless of how many physical resources it were given? Granted, this is necessarily a counterfactual, but . . .

I am not a platonist, but I still can't call myself a formalist, because I can't bring myself to declare confidently that the TPC would become meaningless if it were proved undecidable in ZFC. Indeed, even if the TPC happens to be undecidable in every formal system whose axioms would seem to us to be "intuitively correct" of numbers, it still seems to me that our concept of number may suffice to determine a truth value for the above counterfactual. Either that computer would churn out pairs forever, or it wouldn't.