The set of universally valid formulas of first-order logic becomes such an example if you index formulas by natural numbers in a computable way. This is called Church's theorem, after Alonzo Church. He proved this in the 1930s. This means that although there is a fast proof-checking algorithm, there is no fast proof-finding algorithm.
The set of polynomial equations in several variables with integer coefficients that have integer solutions is another such example. That's called Matiyasevich's theorem. It was proved in 1970 by Uri Matiyasevich, who built on earlier work of Julia Robinson, Hillary Putnam, and Martin Davis. It disposed of Hilbert's tenth problem.