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 $\mathbf{TC}^0$-Frege. This extends the line of results of Kraj\'i\v{c}ek and Pudl\'ak (Information and Computation, 1998), Bonet, Pitassi, and Ray (FOCS, 1997), and Bonet et al. (Computational Complexity, 2004), who showed that Extended Frege, $\mathbf{TC}^0$-Frege and $\mathbf{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.

翻译：我们证明了量子算法在高效证明搜索中的首个困难性结果。我们表明，在标准格基密码学假设——带误差学习（LWE）下，不存在量子算法能够弱自动化 $\mathbf{TC}^0$-弗雷格系统。这一结果拓展了Krajíček和Pudlák（1998年《信息与计算》）、Bonet、Pitassi和Ray（1997年FOCS会议）以及Bonet等人（2004年《计算复杂性》）的研究脉络，他们分别证明了若RSA密码系统或Diffie-Hellman密钥交换协议安全，则扩展弗雷格系统、$\mathbf{TC}^0$-弗雷格系统和$\mathbf{AC}^0$-弗雷格系统无法被经典算法弱自动化。据我们所知，这是量子计算与命题证明搜索的首次交互。