{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T05:37:01Z","timestamp":1777354621193,"version":"3.51.4"},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T00:00:00Z","timestamp":1761523200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T00:00:00Z","timestamp":1761523200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["comput. complex."],"published-print":{"date-parts":[[2025,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We prove the first hardness results against efficient proof search by quantum algorithms. We show that under\nLearning with Errors (LWE), the standard lattice-based cryptographic assumption, no quantum algorithm can weakly\nautomate\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$${\\rm TC}^0$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow>\n                              <mml:mi>TC<\/mml:mi>\n                            <\/mml:mrow>\n                            <mml:mn>0<\/mml:mn>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -Frege. This extends the line of results of Kraj\u00ed\u00ed\u010dek and Pudl\u00edk(\n                    <jats:italic>Information and Computation<\/jats:italic>\n                    , 1998), Bonet, Pitassi, and Raz (\n                    <jats:italic>SIAM Journal on Computing<\/jats:italic>\n                    , 2000),and Bonet, Domingo, Gavald\u00e1, Maciel, and Pitassi (\n                    <jats:italic>Computational Complexity, 2004<\/jats:italic>\n                    ), who showed that ExtendedFrege,\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$${\\rm TC}^0$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow>\n                              <mml:mi>TC<\/mml:mi>\n                            <\/mml:mrow>\n                            <mml:mn>0<\/mml:mn>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -Frege and\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$${\\rm AC}^0$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:msup>\n                            <mml:mrow>\n                              <mml:mi>AC<\/mml:mi>\n                            <\/mml:mrow>\n                            <mml:mn>0<\/mml:mn>\n                          <\/mml:msup>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -Frege, respectively, cannot be weakly automated by classical algorithms if\neither the RSA cryptosystem or the Diffie-Hellman key exchange protocol are secure. To the best of our knowledge,\nthis is the first interaction between quantum computation and propositional proof search.\n                  <\/jats:p>","DOI":"10.1007\/s00037-025-00271-w","type":"journal-article","created":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T09:51:54Z","timestamp":1761558714000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Quantum Automating TC0-Frege Is LWE-Hard"],"prefix":"10.1007","volume":"34","author":[{"given":"Noel","family":"Arteche","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gaia","family":"Carenini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthew","family":"Gray","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,10,27]]},"reference":[{"key":"271_CR1","doi-asserted-by":"crossref","unstructured":"Dorit Aharonov & Oded Regev (2005). Lattice problems in NP\u2229\ncoNP. Journal of the ACM (JACM) 52(5), 749\u2013765.","DOI":"10.1145\/1089023.1089025"},{"key":"271_CR2","doi-asserted-by":"crossref","unstructured":"Mikl\u00f3s Ajtai (1996). Generating hard instances of lattice problems.\nIn Proceedings of the twenty-eighth annual ACM symposium on Theory\nof computing, 99\u2013108.","DOI":"10.1145\/237814.237838"},{"key":"271_CR3","doi-asserted-by":"crossref","unstructured":"Mikl\u00f3s Ajtai & Cynthia Dwork (1997). A public-key cryptosystem\nwith worst-case\/average-case equivalence. In Proceedings of the twentyninth\nannual ACM symposium on Theory of computing, 284\u2013293.","DOI":"10.1145\/258533.258604"},{"key":"271_CR4","doi-asserted-by":"crossref","unstructured":"M. Alekhnovich, M. Braverman, V. Feldman, A.R. Klivans &\nT. Pitassi (2004). Learnability and automatizability. In 45th Annual\nIEEE Symposium on Foundations of Computer Science, 621\u2013630.","DOI":"10.1109\/FOCS.2004.36"},{"key":"271_CR5","doi-asserted-by":"crossref","unstructured":"Michael Alekhnovich, Samuel R. Buss, Shlomo Moran & Toniann\nPitassi (2001). Minimum Propositional Proof Length Is-Hard\nto Linearly Approximate. Journal of Symbolic Logic 66(1), 171\u2013191.","DOI":"10.2307\/2694916"},{"key":"271_CR6","doi-asserted-by":"crossref","unstructured":"Michael Alekhnovich & Alexander A Razborov (2008). Resolution\nis not automatizable unless W[P] is tractable. SIAM Journal on\nComputing 38(4), 1347\u20131363.","DOI":"10.1137\/06066850X"},{"key":"271_CR7","unstructured":"Sanjeev Arora & Boaz Barak (2009). Computational Complexity:\nA Modern Approach. Cambridge University Press. ISBN 978-0-\n521-42426-4."},{"key":"271_CR8","unstructured":"Noel Arteche, Gaia Carenini & Matthew Gray (2024). Quantum\nAutomating $${\\bf TC^{0}}$$-Frege Is LWE-Hard. In 39th Computational\nComplexity Conference, CCC 2024, July 22-25, 2024, Ann Arbor, MI,\nUSA, 15:1\u201315:25."},{"key":"271_CR9","doi-asserted-by":"crossref","unstructured":"Albert Atserias & Mar\u00eda Luisa Bonet (2004). On the automatizability\nof resolution and related propositional proof systems. Information\nand Computation 189(2), 182\u2013201.","DOI":"10.1016\/j.ic.2003.10.004"},{"key":"271_CR10","doi-asserted-by":"crossref","unstructured":"Albert Atserias & Elitza Maneva (2011). Mean-payoff games and\npropositional proofs. Information and Computation 209(4), 664\u2013691.","DOI":"10.1016\/j.ic.2011.01.003"},{"key":"271_CR11","doi-asserted-by":"crossref","unstructured":"Albert Atserias & Moritz M\u00fcller (2020). Automating resolution\nis NP-hard. Journal of the ACM (JACM) 67(5), 1\u201317.","DOI":"10.1145\/3409472"},{"key":"271_CR12","doi-asserted-by":"crossref","unstructured":"Wojciech Banaszczyk (1993). New bounds in some transference theorems\nin the geometry of numbers. Mathematische Annalen 296, 625\u2013\n635.","DOI":"10.1007\/BF01445125"},{"key":"271_CR13","doi-asserted-by":"crossref","unstructured":"P. Beame & T. Pitassi (1996). Simplified and improved resolution\nlower bounds. In Proceedings of 37th Conference on Foundations of\nComputer Science, 274\u2013282.","DOI":"10.1109\/SFCS.1996.548486"},{"key":"271_CR14","doi-asserted-by":"crossref","unstructured":"Arnold Beckmann, Pavel Pudl\u00e1k & Neil Thapen (2014). Parity\ngames and propositional proofs. ACM Transactions on Computational\nLogic (TOCL) 15(2), 17:1\u201317:30.","DOI":"10.1145\/2579822"},{"key":"271_CR15","unstructured":"Zo\u00eb Bell (2020). Automating regular or ordered resolution is NP-hard.\nElectronic Colloquium on Computational Complexity (ECCC)(TR20-105). URL \nhttps:\/\/eccc.weizmann.ac.il\/report\/2020\/105."},{"key":"271_CR16","unstructured":"Huck Bennett & Chris Peikert (2023). Hardness of the (Approximate)\nShortest Vector Problem: A Simple Proof via Reed-Solomon\ncodes. In Approximation, Randomization, and Combinatorial Optimization.\nAlgorithms and Techniques, APPROX\/RANDOM 2023, volume\n275, 37:1\u201337:20."},{"key":"271_CR17","doi-asserted-by":"crossref","unstructured":"Mar\u00eda Luisa Bonet, Carlos Domingo, Ricard Gavald\u00e0, Alexis\nMaciel & Toniann Pitassi (2004). Non-automatizability of boundeddepth\nFrege proofs. computational complexity 13, 47\u201368.","DOI":"10.1007\/s00037-004-0183-5"},{"key":"271_CR18","doi-asserted-by":"crossref","unstructured":"Mar\u00eda Luisa Bonet, Toniann Pitassi & Ran Raz (2000). On interpolation\nand automatization for Frege systems. SIAM Journal on\nComputing 29(6), 1939\u20131967.","DOI":"10.1137\/S0097539798353230"},{"key":"271_CR19","doi-asserted-by":"crossref","unstructured":"Sam Buss & Jakob Nordstr\u00f6m (2021). Proof Complexity and SAT\nSolving. Handbook of Satisfiability 233\u2013350.","DOI":"10.3233\/FAIA200990"},{"key":"271_CR20","doi-asserted-by":"crossref","unstructured":"Samuel R Buss (1995). On G\u00f6del\u2019s theorems on lengths of proofs. II.\nLower bounds for recognizing $$k$$ symbol provability. In Feasible mathematics\nII, 57\u201390. Springer.","DOI":"10.1007\/978-1-4612-2566-9_4"},{"key":"271_CR21","doi-asserted-by":"crossref","unstructured":"Stephen Cook & Phuong Nguyen (2010). Logical Foundations of\nProof Complexity. Cambridge University Press.","DOI":"10.1017\/CBO9780511676277"},{"key":"271_CR22","doi-asserted-by":"crossref","unstructured":"Stephen A. Cook & Robert A. Reckhow (1979). The Relative\nEfficiency of Propositional Proof Systems. J. Symb. Log.  44(1), 36\u201350.","DOI":"10.2307\/2273702"},{"key":"271_CR23","doi-asserted-by":"crossref","unstructured":"Stefan Dantchev, Barnaby Martin & Stefan Szeider (2011).\nParameterized proof complexity. Computational Complexity  20, 51\u201385.","DOI":"10.1007\/s00037-010-0001-1"},{"key":"271_CR24","unstructured":"Michal Garl\u00edk (2024). Failure of Feasible Disjunction Property for\n$$k$$-DNF Resolution and  NP-Hardness of Automating It. In 39th Computational\nComplexity Conference, CCC 2024, July 22-25, 2024, Ann\nArbor, MI, USA, volume 300, 33:1\u201333:23."},{"key":"271_CR25","doi-asserted-by":"crossref","unstructured":"Mika G\u00f6\u00f6s, Sajin Koroth, Ian Mertz & Toniann Pitassi (2020).\nAutomating cutting planes is NP-hard. In Proceedings of the 52nd Annual\nACM SIGACT Symposium on Theory of Computing, 68\u201377.","DOI":"10.1145\/3357713.3384248"},{"key":"271_CR26","doi-asserted-by":"crossref","unstructured":"Rishab Goyal, Venkata Koppula, Satyanarayana Vusirikala\n& Brent Waters (2020). On perfect correctness in (lockable) obfuscation.\nIn Theory of Cryptography - 18th International Conference, TCC\n2020, Durham, NC, USA, November 16-19, 2020, Proceedings, Part I,\n229\u2013259.","DOI":"10.1007\/978-3-030-64375-1_9"},{"key":"271_CR27","doi-asserted-by":"crossref","unstructured":"Lov K Grover (1996). A fast quantum mechanical algorithm for\ndatabase search. In Proceedings of the twenty-eighth annual ACM symposium\non Theory of computing, 212\u2013219.","DOI":"10.1145\/237814.237866"},{"key":"271_CR28","doi-asserted-by":"crossref","unstructured":"Lei Huang & Toniann Pitassi (2011). Automatizability and simple\nstochastic games. In Automata, Languages and Programming - 38th\nInternational Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8,\n2011, Proceedings, Part I, 605\u2013617.","DOI":"10.1007\/978-3-642-22006-7_51"},{"key":"271_CR29","unstructured":"Dmitry Itsykson & Artur Riazanov (2022). Automating OBDD\nproofs is NP-hard. In 47th International Symposium on Mathematical\nFoundations of Computer Science (MFCS 2022), volume 241, 59:1\u2013\n59:15."},{"key":"#cr-split#-271_CR30.1","doi-asserted-by":"crossref","unstructured":"Kazuo Iwama (1997). Complexity of finding short resolution proofs.","DOI":"10.1007\/BFb0029974"},{"key":"#cr-split#-271_CR30.2","unstructured":"In Mathematical Foundations of Computer Science 1997, 309-318."},{"key":"271_CR31","unstructured":"Emil Je\u0159\u00e1bek (2005). Weak pigeonhole principle, and randomized\ncomputation. Ph.D. thesis, Faculty of Mathematics and Physics, Charles\nUniversity, Prague."},{"key":"271_CR32","doi-asserted-by":"crossref","unstructured":"Emil Je\u0159\u00e1bek (2023). Elementary analytic functions in $$\\sf VTC\\it ^0$$. Annals\nof Pure and Applied Logic 174(6), 103 269.","DOI":"10.1016\/j.apal.2023.103269"},{"key":"271_CR33","doi-asserted-by":"crossref","unstructured":"Jan Kraj\u00ed\u010dcek (1995). Bounded Arithmetic, Propositional Logic and\nComplexity Theory. Cambridge University Press.","DOI":"10.1017\/CBO9780511529948"},{"key":"271_CR34","doi-asserted-by":"crossref","unstructured":"Jan Kraj\u00ed\u010dcek (1997). Interpolation theorems, lower bounds for proof\nsystems, and independence results for bounded arithmetic. The Journal\nof Symbolic Logic 62(2), 457\u2013486.","DOI":"10.2307\/2275541"},{"key":"271_CR35","unstructured":"Jan Kraj\u00ed\u010dcek (2019). Proof Complexity. Cambridge University Press."},{"key":"271_CR36","doi-asserted-by":"crossref","unstructured":"Jan Kraj\u00ed\u010dcek (2022). Information in propositional proofs and algorithmic\nproof search. The Journal of Symbolic Logic 87(2), 852\u2013869.","DOI":"10.1017\/jsl.2021.75"},{"key":"271_CR37","doi-asserted-by":"crossref","unstructured":"Jan Kraj\u00ed\u010dcek & Pavel Pudl\u00e1k (1998). Some Consequences of Cryptographical\nConjectures for $$\\sf S\\it _2^1$$\nand EF. Information and Computation\n140(1), 82\u201394.","DOI":"10.1006\/inco.1997.2674"},{"key":"271_CR38","unstructured":"Ian Mertz, Toniann Pitassi & Yuanhao Wei (2019). Short proofs\nare hard to find. In 46th International Colloquium on Automata, Languages,\nand Programming (ICALP 2019), volume 132, 84:1\u201384:16."},{"key":"271_CR39","doi-asserted-by":"crossref","unstructured":"Daniele Micciancio (2011). The Geometry of Lattice Cryptography,\n185\u2013210. Springer Berlin, Heidelberg.","DOI":"10.1007\/978-3-642-23082-0_7"},{"key":"271_CR40","doi-asserted-by":"crossref","unstructured":"Daniele Micciancio & Chris Peikert (2012). Trapdoors for lattices:\nSimpler, tighter, faster, smaller. In Annual International Conference\non the Theory and Applications of Cryptographic Techniques,\n700\u2013718. Springer.","DOI":"10.1007\/978-3-642-29011-4_41"},{"key":"271_CR41","unstructured":"Theodoros Papamakarios (2024). Depth-d Frege Systems Are Not\nAutomatable Unless $$\\bf P\\it  = \\bf NP\\it $$. In 39th Computational Complexity Conference\n(CCC 2024), volume 300, 22:1\u201322:17."},{"key":"271_CR42","doi-asserted-by":"crossref","unstructured":"Chris Peikert (2016). A decade of lattice cryptography. Foundations\nand Trends in Theoretical Computer Science 10(4), 283\u2013424.","DOI":"10.1561\/0400000074"},{"key":"271_CR43","doi-asserted-by":"crossref","unstructured":"Chris Peikert & Brent Waters (2008). Lossy trapdoor functions\nand their applications. In Proceedings of the fortieth annual ACM symposium\non Theory of computing, 187\u2013196.","DOI":"10.1145\/1374376.1374406"},{"key":"271_CR44","unstructured":"J\u00e1n Pich & Rahul Santhanam (2022). Learning Algorithms Versus\nAutomatability of Frege Systems. In 49th International Colloquium on\nAutomata, Languages, and Programming (ICALP 2022), volume 229,\n101:1\u2013101:20."},{"key":"271_CR45","doi-asserted-by":"crossref","unstructured":"Pavel Pudl\u00e1k (2009). Quantum deduction rules. Annals of Pure and\nApplied Logic 157(1), 16\u201329.","DOI":"10.1016\/j.apal.2008.09.017"},{"key":"271_CR46","doi-asserted-by":"crossref","unstructured":"Pavel Pudl\u00e1k (2003). On reducibility and symmetry of disjoint NP\npairs. Theoretical Computer Science 295(1), 323\u2013339.","DOI":"10.1016\/S0304-3975(02)00411-5"},{"key":"271_CR47","unstructured":"Nael Rahman & Vladimir Shpilrain (2021). MOBS (Matrices Over\nBit Strings) public key exchange."},{"key":"271_CR48","doi-asserted-by":"crossref","unstructured":"Oded Regev (2009). On lattices, learning with errors, random linear\ncodes, and cryptography. Journal of the ACM (JACM) 56(6), 1\u201340.","DOI":"10.1145\/1568318.1568324"},{"key":"271_CR49","doi-asserted-by":"crossref","unstructured":"Susanna F. de Rezende, Mika G\u00f6\u00f6s, Jakob Nordstr\u00f6m, Toniann\nPitassi, Robert Robere & Dmitry Sokolov (2021). Automating\nAlgebraic Proof Systems is NP-hard. In Proceedings of the\n53rd Annual ACM SIGACT Symposium on Theory of Computing, 209\u2013\n222.","DOI":"10.1145\/3406325.3451080"},{"key":"271_CR50","doi-asserted-by":"crossref","unstructured":"P.W. Shor (1994). Algorithms for quantum computation: discrete\nlogarithms and factoring. In Proceedings 35th Annual Symposium on\nFoundations of Computer Science, 124\u2013134.","DOI":"10.1109\/SFCS.1994.365700"},{"key":"271_CR51","doi-asserted-by":"crossref","unstructured":"Michael Soltys & Stephen Cook (2004). The proof complexity\nof linear algebra. Annals of Pure and Applied Logic 130(1), 277\u2013323.\nPapers presented at the 2002 IEEE Symposium on Logic in Computer\nScience (LICS).","DOI":"10.1016\/j.apal.2003.10.018"},{"key":"#cr-split#-271_CR52.1","unstructured":"A. Chi-Chih Yao (1993). Quantum circuit complexity. In Proceedings"},{"key":"#cr-split#-271_CR52.2","unstructured":"of 1993 IEEE 34th Annual Foundations of Computer Science, 352-361."}],"container-title":["computational complexity"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00037-025-00271-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00037-025-00271-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00037-025-00271-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,3]],"date-time":"2025-12-03T17:00:19Z","timestamp":1764781219000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00037-025-00271-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,27]]},"references-count":54,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["271"],"URL":"https:\/\/doi.org\/10.1007\/s00037-025-00271-w","relation":{},"ISSN":["1016-3328","1420-8954"],"issn-type":[{"value":"1016-3328","type":"print"},{"value":"1420-8954","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,27]]},"assertion":[{"value":"12 December 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 July 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 October 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"16"}}