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 Raz (FOCS, 1997), and Bonet, Domingo, Gavald\`a, Maciel, and Pitassi (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$-Frege。这扩展了 Krajíček 与 Pudlák（Information and Computation, 1998）、Bonet、Pitassi 与 Raz（FOCS, 1997）以及 Bonet、Domingo、Gavaldà、Maciel 与 Pitassi（Computational Complexity, 2004）的研究成果，他们分别证明了如果 RSA 密码系统或 Diffie-Hellman 密钥交换协议是安全的，则经典算法无法弱自动化 Extended Frege、$\mathbf{TC}^0$-Frege 和 $\mathbf{AC}^0$-Frege。据我们所知，这是量子计算与命题证明搜索领域的首次交叉研究。