Abstract

We prove the first hardness results against efficient proof search by quantum

algorithms. We show that under Learning with Errors (LWE), the standard

lattice-based cryptographic assumption, no quantum algorithm can weakly

automate TC⁰-Frege. This extends the line of results of Krajíček and

Pudlák (Information and Computation, 1998), Bonet, Pitassi, and Raz (FOCS,

1997), and Bonet, Domingo, Gavaldà, Maciel, and Pitassi (Computational

Complexity, 2004), who showed that Extended Frege, TC⁰-Frege and AC⁰-Frege,

respectively, cannot be weakly automated by classical algorithms if either 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.



This is joint work with Gaia Carenini and Matthew Gray.