We consider the proof search ("automatizability") problem for integrated learning and reasoning, a problem modeling certain kinds of data mining and common sense reasoning (Juba, 2013a). In such a problem, the approximate validity (i.e., under Valiant’s PAC-Semantics (Valiant, 2000)) of an input query formula over a background probability distribution is verified using incomplete examples from the distribution; queries featuring a proof from some learnable premises are distinguished from queries that are falsified with moderately high probability under the distribution. The introduction of tolerance for some approximation and examples from the target distribution raise the possibility that this problem may be easier than classical automatizability in many circumstances. In particular, for certain restricted distributions and information-masking processes, the automatizability problem for resolution can be solved in quasipolynomial time (Juba, 2013b). Nevertheless, we argue here that the known cryptographic non-automatizability results (Krajicek and Pudlak 1995; Bonet, Pitassi, and Raz 2000; Bonet et al. 2004) carry over to even the highly restricted kinds of distributions considered in that work.