What are some things we can prove they must exist, but have no idea what they are?

Not sure if this satisfies the requirement that we "have no idea what they are", but the extremely strange Mill's constant seems worth mentioning here: There is supposed to be some real number $r>0$ with the property that the integer part of $$r^{3^n}$$ is prime for every natural $n$. It is not known if $r$ is rational and as far as I know not even a numerical approximation of $r$ is possible without assuming the Riemann hypothesis.

Source: Wikipedia

There are a number of games, like Hex and Chomp, for which it is easy to prove a first player win by strategy stealing but we do not generally know the winning strategy.

Take objects which existence proof uses the axiom of choice, e.g:

• Each vector space has a basis (the standard existence proof uses Zorn's lemma). How does a concrete basis of $C[a,b]$ look like? What about $\mathbb R$ as a $\mathbb Q$-vector space?
• Ultrafilter, which are used in the construction of the hyperreals: Does the sequence $(0,1,0,1,0,1,\ldots)$ represent $0$ or $1$? The answer to this question depends on the chosen ultrafilter, but its existence proof uses the axiom of choice...

Well defined numbers for which only estimations are currently known:

• Ramsey numbers.

The leading (decimal) digit of the ludicrously huge number $TREE(3)$. (See https://cp4space.wordpress.com/2012/12/19/fast-growing-2/ and http://www.cs.nyu.edu/pipermail/fom/2006-March/010279.html.)

OK, one might object "But that's an absolutely uninteresting object!" That may be; I'd argue, though, that it is meta-interesting in the following sense. The problem

Determine the leading digit of $TREE(n)$

is, I think, likely to be extremely hard - I would bet my entire life savings that it is not in $P$, $NP$, $EXP$, . . . or really any reasonable complexity class at all, simply because in order to compute it we seem to have to compute $TREE(n)$. But as far as I know, proving that we need to do this (let alone making clear what we mean by this) is galactically out of reach, and I would be extremely surprised if I lived to see even a proof that the problem is not linear-time computable.

So I'd argue that the leading digits of such huge numbers are interesting as a class, even if individually they're a bit pointless, because they represent a really weird kind of intractable computation.

A partition of the 3D ball into 5 distinct pieces such that, through only translations and rotations, the pieces can be moved and reassembled into two balls, each of equal size to the original.

This is the Banach-Tarski paradox. The existence of such a partition depends on the axiom of choice, so in particuar there is no way to say exactly what the partition looks like, other than the fact that one exists.