Quantum Automating TC0-Frege Is LWE-Hard
Noel Arteche, Gaia Carenini, Matthew Gray · Computational Complexity · 2025
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$$ 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$$ TC 0 -Frege and $${\rm AC}^0$$ AC 0 -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.