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:
Well defined numbers for which only estimations are currently known: