{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:59:28Z","timestamp":1781078368276,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,6,15]],"date-time":"2021-06-15T00:00:00Z","timestamp":1623715200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"European Union's Horizon 2020 research and innovation programme under the Marie Sklodovska-Curie grant agreement","award":["890220"],"award-info":[{"award-number":["890220"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,6,15]]},"DOI":"10.1145\/3406325.3451117","type":"proceedings-article","created":{"date-parts":[[2021,6,16]],"date-time":"2021-06-16T01:26:13Z","timestamp":1623806773000},"page":"223-233","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Strong co-nondeterministic lower bounds for NP cannot be proved feasibly"],"prefix":"10.1145","author":[{"given":"J\u00e1n","family":"Pich","sequence":"first","affiliation":[{"name":"Czech Academy of Sciences, Czechia \/ University of Oxford, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rahul","family":"Santhanam","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,6,15]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"SIAM Journal on Computing, 34 ( 1 ): 67-88","author":"Alekhnovich M.","year":"2004","unstructured":"Alekhnovich M., Ben-Sasson E., Razborov A.A., Wigderson A. ; Pseudorandom generators in propositional proof complexity, SIAM Journal on Computing, 34 ( 1 ): 67-88, 2004."},{"key":"e_1_3_2_1_2_1","volume-title":"Transactions in Computation Theory, 2 : 1-54","author":"Aaronson S.","year":"2009","unstructured":"Aaronson, S., Wigderson, A. ; Algebrization: A New Barrier in Complexity Theory, Transactions in Computation Theory, 2 : 1-54, 2009."},{"key":"e_1_3_2_1_3_1","first-page":"431","volume-title":"SIAM Journal on Computing, 4 ( 4 )","author":"Baker T.","year":"1975","unstructured":"Baker T., Gill J., Solovay R. ; Relativizations of the P = NP Question, SIAM Journal on Computing, 4 ( 4 ), pp. 431-442, 1975."},{"key":"e_1_3_2_1_4_1","unstructured":"Buss S. ; Bounded Arithmetic Bibliopolis 1986."},{"key":"e_1_3_2_1_5_1","volume-title":"Journal of Symbolic Logic, 49 : 496-525","author":"Buss S.","year":"2014","unstructured":"Buss S., Ko\u0142odziejczyk L., Thapen N. ; Fragments of Approximate Counting, Journal of Symbolic Logic, 49 : 496-525, 2014."},{"key":"e_1_3_2_1_6_1","volume-title":"127-147","author":"Byd\u017eovsk\u00fd J.","year":"2020","unstructured":"Byd\u017eovsk\u00fd J., M\u00fcller M. ; Polynomial time ultrapowers and the consistency of circuit lower bounds, Arch. Math. Log., 59 ( 1 ): 127-147, 2020."},{"key":"e_1_3_2_1_7_1","volume-title":"Logical Methods in Computer Science, 16 ( 2 :12)","author":"Byd\u017eovsk\u00fd J.","year":"2020","unstructured":"Byd\u017eovsk\u00fd J., Kraj\u00ed\u010dek J., Oliveira I.C. ; Consistency of circuit lower bounds with bounded theories, Logical Methods in Computer Science, 16 ( 2 :12), 2020."},{"key":"e_1_3_2_1_8_1","volume-title":"Conference on Computational Complexity, 10 : 1-24","author":"Carmosino M.","year":"2016","unstructured":"Carmosino M., Impagliazzo R., Kabanets V., Kolokolova A. ; Learning algorithms from natural proofs, Conference on Computational Complexity, 10 : 1-24, 2016."},{"key":"e_1_3_2_1_9_1","volume-title":"Innovations in Theoretical Computer Science, 70 : 1-48","author":"Chen L.","year":"2020","unstructured":"Chen L., Hirahara S., Oliveira I.C., Pich J., Rajgopal N., Santhanam R. ; Beyond natural proofs: hardness magnification and locality, Innovations in Theoretical Computer Science, 70 : 1-48, 2020."},{"key":"e_1_3_2_1_10_1","first-page":"24","volume-title":"International Congress of Logic, Methodology and Philosophy of Science, North Holland","author":"Cobham A.","year":"1965","unstructured":"Cobham A. ; The intrinsic computational dificulty of functions, International Congress of Logic, Methodology and Philosophy of Science, North Holland, pp. 24-30, 1965."},{"key":"e_1_3_2_1_11_1","first-page":"83","volume-title":"Symposium on the Theory of Computing","author":"Cook S.A.","year":"1975","unstructured":"Cook S.A. ; Feasibly constructive proofs and the propositional calculus, Symposium on the Theory of Computing, pp. 83-97, 1975."},{"key":"e_1_3_2_1_12_1","volume-title":"Journal of Symbolic Logic, 72 ( 4 ): 1353-1371","author":"Cook S.","year":"2007","unstructured":"Cook S., Kraj\u00ed\u010dek J.; Consequences of the Provability of NP \u2286 P\/poly, Journal of Symbolic Logic, 72 ( 4 ): 1353-1371, 2007."},{"key":"e_1_3_2_1_13_1","volume-title":"Information Processing Letters, 34 ( 2 ): 81-85","author":"Cook S.A.","year":"1990","unstructured":"Cook S.A., Pitassi T. ; A feasibly constructive lower bound for Resolution proofs, Information Processing Letters, 34 ( 2 ): 81-85, 1990."},{"key":"e_1_3_2_1_14_1","volume-title":"ACM Transactions on Computational Logic, 7 ( 4 ): 749-764","author":"Cook S.A.","year":"2006","unstructured":"Cook S.A., Thapen N.; The strength of replacement in weak arithmetic, ACM Transactions on Computational Logic, 7 ( 4 ): 749-764, 2006."},{"key":"e_1_3_2_1_15_1","volume-title":"thesis","author":"Dai Tri Man Le","year":"2014","unstructured":"Dai Tri Man Le ; Bounded arithmetic and formalizing probabilistic proofs, Ph.D. thesis, University of Toronto, 2014."},{"key":"e_1_3_2_1_16_1","volume-title":"International Colloquium on Automata, Languages and Programming, 6755 : 618-629","author":"Filmus Y.","year":"2011","unstructured":"Filmus Y., Pitassi T., Santhanam R. ; Exponential lower bounds for AC0-Frege imply superpolynomial Frege lower bounds, International Colloquium on Automata, Languages and Programming, 6755 : 618-629, 2011."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007352.1007389"},{"key":"e_1_3_2_1_18_1","volume-title":"Arxiv preprint","author":"Huang H.","year":"2019","unstructured":"Huang H. ; Induced Subgraphs of Hypercubes and a Proof of the Sensitivity Conjecture, Arxiv preprint, 2019."},{"key":"e_1_3_2_1_19_1","volume-title":"Annals of Pure and Applied Logic, 129 : 1-37","author":"Je\u0159\u00e1bek E.","year":"2004","unstructured":"Je\u0159\u00e1bek E. ; Dual weak pigeonhole principle, Boolean complexity and derandomization, Annals of Pure and Applied Logic, 129 : 1-37, 2004."},{"key":"e_1_3_2_1_20_1","volume-title":"thesis","author":"Je\u0159\u00e1bek E.","year":"2005","unstructured":"Je\u0159\u00e1bek E. ; Weak pigeonhole principle and randomized computation, Ph.D. thesis, Charles University in Prague, 2005."},{"key":"e_1_3_2_1_21_1","volume-title":"Journal of Symbolic Logic, 72 : 959-993","author":"Je\u0159\u00e1bek E.","year":"2007","unstructured":"Je\u0159\u00e1bek E. ; Approximate counting in bounded arithmetic, Journal of Symbolic Logic, 72 : 959-993, 2007."},{"key":"e_1_3_2_1_22_1","volume-title":"propositional logic, and complexity theory","author":"Kraj\u00ed\u010dek J.","year":"1995","unstructured":"Kraj\u00ed\u010dek J.; Bounded arithmetic, propositional logic, and complexity theory, Cambridge University Press, 1995."},{"key":"e_1_3_2_1_23_1","volume-title":"123-140","author":"Kraj\u00ed\u010dek J.","year":"2001","unstructured":"Kraj\u00ed\u010dek J. ; On the weak pigeonhole principle, Fundamenta Mathematicae, 170 ( 1-3 ): 123-140, 2001."},{"key":"e_1_3_2_1_24_1","volume-title":"Journal of Symbolic Logic, 69 ( 1 ): 265-286","author":"Kraj\u00ed\u010dek J.","year":"2004","unstructured":"Kraj\u00ed\u010dek J.; Dual weak pigeonhole principle, pseudor-surjective functions, and provability of circuit lower bounds, Journal of Symbolic Logic, 69 ( 1 ): 265-286, 2004."},{"key":"e_1_3_2_1_25_1","volume-title":"Journal of Symbolic Logic, 69 ( 2 ): 387-397","author":"Kraj\u00ed\u010dek J.","year":"2004","unstructured":"Kraj\u00ed\u010dek J.; Implicit proofs, Journal of Symbolic Logic, 69 ( 2 ): 387-397, 2004."},{"key":"e_1_3_2_1_26_1","volume-title":"Journal of Mathematical Logic, 11 ( 1 ): 11-27","author":"Kraj\u00ed\u010dek J.","year":"2011","unstructured":"Kraj\u00ed\u010dek J. ; On the proof complexity of the Nisan-Wigderson generator based on a hard NP \u2229 coNP function, Journal of Mathematical Logic, 11 ( 1 ): 11-27, 2011."},{"key":"e_1_3_2_1_27_1","volume-title":"Bulleting of the London Mathematical Society, 46 ( 1 ): 111-125","author":"Kraj\u00ed\u010dek J.","year":"2014","unstructured":"Kraj\u00ed\u010dek J. ; On the computational complexity of finding hard tautologies, Bulleting of the London Mathematical Society, 46 ( 1 ): 111-125, 2014."},{"key":"e_1_3_2_1_28_1","volume-title":"Cambridge University Press","author":"Kraj\u00ed\u010dek J.","year":"2019","unstructured":"Kraj\u00ed\u010dek J. ; Proof complexity, Cambridge University Press, 2019."},{"key":"e_1_3_2_1_29_1","volume-title":"Logical Methods in Computer Science, 16 ( 3 :9)","author":"Kraj\u00ed\u010dek J.","year":"2020","unstructured":"Kraj\u00ed\u010dek J.; A limitation on the KPT interpolation, Logical Methods in Computer Science, 16 ( 3 :9), 2020."},{"key":"e_1_3_2_1_30_1","volume-title":"Logical Methods in Computer Science, 13 ( 1 )","author":"Kraj\u00ed\u010dek J.","year":"2017","unstructured":"Kraj\u00ed\u010dek J., Oliveira I.C. ; Unprovability of circuit upper bounds in Cook's theory PV1, Logical Methods in Computer Science, 13 ( 1 ), 2017."},{"key":"e_1_3_2_1_31_1","volume-title":"Information and Computation, 140 ( 1 ): 82-94","author":"Kraj\u00ed\u010dek J.","year":"1998","unstructured":"Kraj\u00ed\u010dek J., Pudl\u00e1k P.; Some consequences of cryptographical conjectures for S12 and EF, Information and Computation, 140 ( 1 ): 82-94, 1998."},{"key":"e_1_3_2_1_32_1","volume-title":"Annals of Pure and Applied Logic, 52 : 143-153","author":"Kraj\u00ed\u010dek J.","year":"1991","unstructured":"Kraj\u00ed\u010dek J., Pudl\u00e1k P., Takeuti G. ; Bounded arithmetic and the polynomial hierarchy, Annals of Pure and Applied Logic, 52 : 143-153, 1991."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/195058.195447"},{"key":"e_1_3_2_1_34_1","volume-title":"Annals of Pure and Applied Logic, 171 ( 2 )","author":"M\u00fcller M.","year":"2020","unstructured":"M\u00fcller M., Pich J.; Feasibly constructive proofs of succinct weak circuit lower bounds, Annals of Pure and Applied Logic, 171 ( 2 ), 2020."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(05)80043-1"},{"key":"e_1_3_2_1_36_1","volume-title":"Methods in Mathematical Logic, 1130 : 317-340","author":"Paris J.","year":"1985","unstructured":"Paris J., Wilkie A. ; Counting problems in bounded arithmetic, Methods in Mathematical Logic, 1130 : 317-340, 1985."},{"key":"e_1_3_2_1_37_1","volume-title":"Mathematical Logic Quarterly, 57 ( 4 )","author":"Pich J.","year":"2011","unstructured":"Pich J. ; Nisan-Wigderson generators in proof systems with forms of interpolation, Mathematical Logic Quarterly, 57 ( 4 ), 2011."},{"key":"e_1_3_2_1_38_1","volume-title":"Annals of Pure and Applied Logic, 166 ( 1 ): 29-45","author":"Pich J.","year":"2015","unstructured":"Pich J.; Circuit lower bounds in bounded arithmetics, Annals of Pure and Applied Logic, 166 ( 1 ): 29-45, 2015."},{"key":"e_1_3_2_1_39_1","volume-title":"Logical Methods in Computer Science, 11 ( 2 )","author":"Pich J.","year":"2015","unstructured":"Pich J. ; Logical Strength of Complexity Theory and a formalization of the PCP theorem in bounded arithmetic, Logical Methods in Computer Science, 11 ( 2 ), 2015."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2019.00080"},{"key":"e_1_3_2_1_41_1","volume-title":"of Symb. Logic, 62 ( 3 ): 981-998","author":"Pudl\u00e1k P.","year":"1997","unstructured":"Pudl\u00e1k P. ; Lower Bounds for Resolution and Cutting Plane proofs and Monotone computations; J. of Symb. Logic, 62 ( 3 ): 981-998, 1997."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2566-9_12"},{"key":"e_1_3_2_1_43_1","volume-title":"Izvestiya of the Russian Academy of Science, 59 : 201-224","author":"Razborov A.A.","year":"1995","unstructured":"Razborov A.A. ; Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic, Izvestiya of the Russian Academy of Science, 59 : 201-224, 1995."},{"key":"e_1_3_2_1_44_1","volume-title":"Annals of Mathematics, 181 ( 2 ): 415-472","author":"Razborov A.A.","year":"2015","unstructured":"Razborov A.A. ; Pseudorandom generators hard for-DNF resolution and polynomial calculus, Annals of Mathematics, 181 ( 2 ): 415-472, 2015."},{"key":"e_1_3_2_1_45_1","volume-title":"Journal of Computer and System Sciences, 55 ( 1 ): 24-35","author":"Razborov A.A.","year":"1997","unstructured":"Razborov A.A., Rudich S.; Natural proofs, Journal of Computer and System Sciences, 55 ( 1 ): 24-35, 1997."},{"key":"e_1_3_2_1_46_1","volume-title":"Journal of Computer and System Sciences, 55 : 204-213","author":"Rudich S.","year":"1997","unstructured":"Rudich S. ; Super-bits, Demi-bits, and NP\/qpoly-natural Proofs, Journal of Computer and System Sciences, 55 : 204-213, 1997."},{"key":"e_1_3_2_1_47_1","volume-title":"Annals of Pure and Applied Logic, 118 ( 1-2 ): 175-195","author":"Thapen N.","year":"2002","unstructured":"Thapen N.; A model-theoretic characterization of the weak pigeonhole principle, Annals of Pure and Applied Logic, 118 ( 1-2 ): 175-195, 2002."},{"key":"e_1_3_2_1_48_1","volume-title":"thesis","author":"Thapen N.","year":"2002","unstructured":"Thapen N.; The weak pigeonhole principle in models of bounded arithmetic, Ph.D. thesis, Oxford University, 2002."}],"event":{"name":"STOC '21: 53rd Annual ACM SIGACT Symposium on Theory of Computing","location":"Virtual Italy","acronym":"STOC '21","sponsor":["SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 53rd Annual ACM SIGACT Symposium on Theory of Computing"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3406325.3451117","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3406325.3451117","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:24:53Z","timestamp":1750195493000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3406325.3451117"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,15]]},"references-count":48,"alternative-id":["10.1145\/3406325.3451117","10.1145\/3406325"],"URL":"https:\/\/doi.org\/10.1145\/3406325.3451117","relation":{},"subject":[],"published":{"date-parts":[[2021,6,15]]},"assertion":[{"value":"2021-06-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}