We prove the first hardness results against efficient proof search by quantum algorithms. We show that underLearning with Errors (LWE), the standard lattice-based cryptographic assumption, no quantum algorithm can weaklyautomate \({\rm TC}^0\) -Frege. This extends the line of results of Krajííček and Pudlík(Information and Computation, 1998), Bonet, Pitassi, and Raz (SIAM Journal on Computing, 2000),and Bonet, Domingo, Gavaldá, Maciel, and Pitassi (Computational Complexity, 2004), who showed that ExtendedFrege, \({\rm TC}^0\) -Frege and \({\rm AC}^0\) -Frege, respectively, cannot be weakly automated by classical algorithms ifeither the RSA cryptosystem or the Diffie-Hellman key exchange protocol are secure. To the best of our knowledge,this is the first interaction between quantum computation and propositional proof search.
