Quantum Automating TC 0 -Frege Is LWE-Hard

Journal article

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 TC0-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, TC0-Frege and AC0-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.

Authors: Arteche, N; Carenini, G; Gray, M

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Springer
• Journal: Computational Complexity
• Volume: 34
• Issue: 2
• Article number: 16
• Publication date: 2025-10-27
• Acceptance date: 2025-07-15
• DOI: 10.1007/s00037-025-00271-w
• EISSN: 1420-8954
• ISSN: 1016-3328
• Language: English
• Keywords: automatability; 68Q01; post-quantum cryptography; 68Q12; 03F20; proof complexity; feasible interpolation