Quantum Automating TC0-Frege Is LWE-Hard

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 $${\rm TC}^0$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mrow> <mml:mi>TC</mml:mi> </mml:mrow> <mml:mn>0</mml:mn> </mml:msup> </mml:math> -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$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mrow> <mml:mi>TC</mml:mi> </mml:mrow> <mml:mn>0</mml:mn> </mml:msup> </mml:math> -Frege and $${\rm AC}^0$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mrow> <mml:mi>AC</mml:mi> </mml:mrow> <mml:mn>0</mml:mn> </mml:msup> </mml:math> -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.