constructive-mathematicslogicphilosophy
In mathematics the existence of a mathematical object is often proved by contradiction without showing how to construct the object.
Does the existence of the object imply that it is at least possible to construct the object?
Or are there mathematical objects that do exist but are impossible to construct?
All of your criticisms are equally valid when applied to.. well, anything. How does a football coach know what a "formation" is, and whether it really applies to football? How does a software engineer know the difference between a "program" and the instructions executed by a computer? How does a dog know that a "frisbee" is something that you can catch in your mouth? How does a general use little flags to signify troop positions, when they are really just flags?
None of this is to say that these are not interesting questions—I personally find them quite fascinating. But saying that they are reasons not to take something seriously is rather antisocial. If a lover stares into your eyes on a moonlit night and professes his or her adoration, do you start measuring oxytocin concentrations?
I do think that many mathematicians are a bit too attached to the Cantorian or Platonist views, and have incorrectly made mathematics out to be about things which are more than what they are—and that starts many arguments unnecessarily (for example, when someone claims that a theorem is true "in all possible universes", as if that meant anything). In my opinion, topos theory provides a better foundation for mathematics in this sense, because it is easier to understand the relationship between semantics, syntax, and the ever-elusive ontology. One speaks of this topos or that topos (or "topic", if you prefer), and never needs to worry about whether something "is" this or "is" that.
One relatively recent paper which I think has helped advance this more enlightened way of thinking is the quantum mechanics paper (heavily inspired by the philosophical work of Heidegger) What is a Thing?. There it is argued that set theory has not quite succeeded in providing the proper background for interpreting the world as it appears to us. The "state space" of physics professes to arrange possible worlds into a set, and runs headfirst into various paradoxes as we realize that our experimental equipment itself changes what is being measured, blurring our picture of how things really work and necessitating the continual introduction of new concepts and interpretations.
In short: perhaps truth, in the pragmatic sense, is more sheaf-like than set-like. But I digress.
If anybody tells you that you should take math seriously because it has figured out, once and for all, the correct way to divide the abstract from the concrete, and has firmly established the foundations for rational thought, then they are too caught up in their subject and you really shouldn't pay attention to them. And, if you really want, you can simply walk away, shaking your head in disappointment that mathematicians have failed to live up to their promise.
But, however seriously you take it, mathematics remains a powerful force in the world. While we're not particularly better than anybody else at explaining what we're talking about, what we are good at is bringing disparate things together under the same semantical umbrella—to a large extent, precisely because we are given the freedom not to explain ourselves. Measure theory, for example, has allowed us to shuttle insights between discrete phenomena and continuous phenomena. Algebra has, for hundreds of years, improved our speed of numerical reasoning by a billion-fold, by knowing when to compute and when to encode. Algebraic geometry has provided a language that is equally at home with basic arithmetic, encryption, signal processing, causality, and phylogenetic trees. And so people keep finding it useful, however many students will stand up angrily in our classes and insist that they don't think it could possibly be useful because something something.
In short, mathematics saves time for certain kinds of projects. If you don't do any of those projects, then of course you don't need to take it seriously. But it's under no obligation to explain itself, particularly not to somebody who thinks he is entitled to answers and "justice". If you find the foundations lacking, then we would love for you to come make a career of improving those foundations. If you are mostly complaining however, then pardon us while we focus on our other students.
There are various ways to interpret the question. One interesting class of examples consists of "speed up" theorems. These generally involve two formal systems, $T_1$ and $T_2$, and family of statements which are provable in both $T_1$ and $T_2$, but for which the shortest formal proofs in $T_1$ are much longer than the shortest formal proofs in $T_2$.
One of the oldest such theorems is due to Gödel. He noticed that statements such as "This theorem cannot be proved in Peano Arithmetic in fewer than $10^{1000}$ symbols" are, in fact, provable in Peano Arithmetic.
Knowing this, we know that we could make a formal proof by cases that examines every Peano Arithmetic formal proof with fewer than $10^{1000}$ symbols and checks that none of them proves the statement. So we can prove indirectly that a formal proof of the statement in Peano Arithmetic exists.
But, because the statement is true, the shortest formal proof of the statement in Peano Arithmetic will in fact require more than $10^{1000}$ symbols. So nobody will be able to write out that formal proof completely. We can replace $10^{1000}$ with any number we wish, to obtain results whose shortest formal proof in Peano arithmetic must have at least that many symbols.
Similarly, if we prefer another formal system such as ZFC, we can consider statements such as "This theorem cannot be proved in ZFC in fewer than $10^{1000}$ symbols". In this way each sufficiently strong formal system will have some results which we know are formally provable, but for which the shortest formal proof in that system is too long to write down.
Best Answer
Really the answer to this question will come down to the way we define the terms "existence" (and "construct"). Going philosophical for a moment, one may argue that constructibility is a priori required for existence, and so ; this, broadly speaking, is part of the impetus for intuitionism and constructivism, and related to the impetus for (ultra)finitism.$^1$ Incidentally, at least to some degree we can produce formal systems which capture this point of view (although the philosophical stance should really be understood as preceding the formal systems which try to reflect them; I believe this was a point Brouwer and others made strenuously in the early history of intuitionism).
A less philosophical take would be to interpret "existence" as simply "provable existence relative to some fixed theory" (say, ZFC, or ZFC + large cardinals). In this case it's clear what "exists" means, and the remaining weasel word is "construct." Computability theory can give us some results which may be relevant, depending on how we interpret this word: there are lots of objects we can define in a complicated way but provably have no "concrete" definitions:
The halting problem is not computable.
Kleene's $\mathcal{O}$ - or, the set of indices for computable well-orderings - is not hyperarithmetic.
A much deeper example: while we know that for all Turing degrees ${\bf a}$ there is a degree strictly between ${\bf a}$ and ${\bf a'}$ which is c.e. in $\bf a$, we can also show that there is no "uniform" way to produce such a degree in a precise sense.
Going further up the ladder, ideas from inner model theory and descriptive set theory become relevant. For example:
We can show in ZFC that there is a (Hamel) basis for $\mathbb{R}$ as a vector space over $\mathbb{Q}$; however, we can also show that no such basis is "nicely definable," in various precise senses (and we get stronger results along these lines as we add large cardinal axioms to ZFC). For example, no such basis can be Borel.
Other examples of the same flavor: a nontrivial ultrafilter on $\mathbb{N}$; a well-ordering of $\mathbb{R}$; a Vitali (or Bernstein or Luzin) set, or indeed any non-measurable set (or set without the property of Baire, or without the perfect set property); ...
On the other side of the aisle, the theory ZFC + a measurable cardinal proves that there is a set of natural numbers which is not "constructible" in a precise set-theoretic sense (basically, can be built just from "definable transfinite recursion" starting with the emptyset). Now the connection between $L$-flavored constructibility and the informal notion of a mathematical construction is tenuous at best, but this does in my opinion say that a measurable cardinal yields a hard-to-construct set of naturals in a precise sense.
$^1$I don't actually hold these stances except very rarely, and so I'm really not the best person to comment on their motivations; please take this sentence with a grain of salt.