Non-constructive existence proofs, which establish the existence of objects without furnishing an efficient algorithm to produce examples, abound in mathematics. How hard is it, computationally, to find objects whose existence is guaranteed non-constructively? Since the 1980's complexity theorists have been classifying these search problems into broad classes of computationally equivalent problems, each corresponding to a different non-constructive proof principle, such as the pigeonhole principle, the local search principle (that any function on a finite graph has a local minimum), and the parity principle (that a finite set of odd cardinality cannot be empty). All of these problems are contained in the complexity class TFNP, consisting of search problems for which a solution is guaranteed to exist and the validity of a solution can be efficiently verified. One of the most successful non-constructive methods for proving existence of combinatorial objects, the probabilistic method, does not seem to be captured by TFNP because the applications of the probabilistic method often yield existence of objects whose properties are hard to verify computationally. For example, Erdos famously used the probabilistic method to prove the existence of "Ramsey graphs" having no large cliques or independent sets; however, it is hard to verify that a given graph is a Ramsey graph. This motivates exploring the complexity of search problems for which existence of solutions is still guaranteed but efficient verification of solutions is no longer possible. Many such problems can be organized into a hierarchy depending on the number of alternating quantifiers in the logical formula that solutions must satisfy. At the second level of the hierarchy we encounter a class that seems especially rich in such problems: PEPP (for “polynomial empty pigeonhole principle”), which includes problems related to probabilistic-method proofs based on the union bound. Examples include finding a bit string that is far from all codewords, finding an explicit rigid matrix, as well as a problem we call Complexity, capturing Complexity Theory’s quest to find functions that cannot be computed by small circuits. When the union bound is generous, in that solutions constitute at least a polynomial fraction of the domain, we have a family of seemingly weaker classes α-PEPP. Higher in the hierarchy, we identify the constructive version of the Sauer-Shelah lemma and the appropriate generalization of PPP that contains it, as well as the problem of finding a king in a tournament (a vertex k such that all other vertices are defeated by k, or by somebody k defeated). Joint work with Oliver Korten, Dan Mitropolsky, and Christos Papadimitriou.