Quantum Automating TC⁰-Frege Is LWE-Hard

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.