There are certain "probabilistic constructions" in Banach space theory where one shows that something happens with positive probability, but where explicit examples still aren't known. (That said, I am not up to speed with the developments here, and I seem to recall reading that in several cases, via derandomization techniques one can turn the existence proofs into reasonable algorithms for producing examples.)

The sort of thing I have in mind is the Johnson-Lindenstrauss lemma, but I can think of at least two regular MO users who would be better placed than me to comment on it.