Quantum Automating ${\mathbf{TC}}^0$-Frege Is LWE-Hard

Noel Arteche, Gaia Carenini, Matthew Gray

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 as…