What are some things we can prove they must exist, but have no idea what they are? What are some things we can prove they must exist, but have no idea what they are?
Examples I can think of:


*

*Values of the Busy beaver function: It is a well-defined function, but not computable.

*It had been long known that there must be self-replicating patterns in Conway's Game of Life, but the first such pattern has only been discovered in 2010

*By the Well-ordering theorem under the assumptions of the axiom of choice, every set admits a well-ordering. (See also Is there a known well ordering of the reals?)


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.

