{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,23]],"date-time":"2026-04-23T16:47:29Z","timestamp":1776962849134,"version":"3.51.4"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"2","funder":[{"DOI":"10.13039\/501100000288","name":"Royal Society","doi-asserted-by":"publisher","award":["URF\/R1\/211106"],"award-info":[{"award-number":["URF\/R1\/211106"]}],"id":[{"id":"10.13039\/501100000288","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2026,4,30]]},"abstract":"<jats:p>\n                    We give a new approach to the fundamental question of whether proof complexity lower bounds for concrete propositional proof systems imply super-polynomial Boolean circuit lower bounds. We observe that any general implication from proof complexity lower bounds for a propositional proof system to super-polynomial Boolean circuit lower bounds implies unconditionally that\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\({\\sf NEXP}\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    does not have Boolean circuits of polynomial size. We explore connections that are possible to establish without settling this long-standing and famously hard open question.\n                  <\/jats:p>\n                  <jats:p>\n                    For any poly-time computable function\n                    <jats:italic toggle=\"yes\">f<\/jats:italic>\n                    , we define the witnessing formulas\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(w_n^k(f)\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    , which are propositional formulas stating that for any circuit\n                    <jats:italic toggle=\"yes\">C<\/jats:italic>\n                    of size\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(n^k\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    on\n                    <jats:italic toggle=\"yes\">n<\/jats:italic>\n                    variables and for any formula\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\phi\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    of size\n                    <jats:italic toggle=\"yes\">n<\/jats:italic>\n                    , either\n                    <jats:italic toggle=\"yes\">C<\/jats:italic>\n                    computes a satisfying assignment to\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(\\phi\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    or\n                    <jats:italic toggle=\"yes\">f<\/jats:italic>\n                    verifiably refutes that\n                    <jats:italic toggle=\"yes\">C<\/jats:italic>\n                    computes\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\({\\sf SAT}\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    on instances of length\n                    <jats:italic toggle=\"yes\">n<\/jats:italic>\n                    . We show that if the witnessing formulas are tautologies, then any super-polynomial lower bound for Extended Frege augmented with\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\(w_n^k(f)\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    axioms implies that\n                    <jats:inline-formula content-type=\"math\/tex\">\n                      <jats:tex-math notation=\"LaTeX\" version=\"MathJax\">\\({\\sf SAT}\\)<\/jats:tex-math>\n                    <\/jats:inline-formula>\n                    requires super-polynomial size Boolean circuits. We also give an unconditional equivalence between circuit lower bounds for the Discrete Logarithm problem and proof complexity lower bounds (for propositional formulas efficiently encoding the statement that the Discrete Logarithm problem is computable by small circuits) for a concretely defined strong (non-uniform) propositional proof system.\n                  <\/jats:p>\n                  <jats:p>\n                    We give consequences of our connections for the meta-mathematics of several major questions in computational complexity, including whether one-way functions can be based on the worst-case hardness of NP, whether there is a dichotomy between one-way functions and worst-case learning with membership queries over the uniform distribution, and whether there are feasibly constructible anti-checkers for Satisfiability. We show that for each of these questions, provability of a positive answer in essentially\n                    <jats:italic toggle=\"yes\">any<\/jats:italic>\n                    standard mathematical theory would imply new connections between propositional proof complexity and circuit complexity.\n                  <\/jats:p>\n                  <jats:p>Our results rely on a new notion of \u201cself-provability\u201d of upper bounds, which might be independently interesting, and involve a novel application of random self-reducibility to proof complexity.<\/jats:p>","DOI":"10.1145\/3801091","type":"journal-article","created":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T20:56:23Z","timestamp":1773953783000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Towards P\u2260NP from Extended Frege lower bounds"],"prefix":"10.1145","volume":"73","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2731-1330","authenticated-orcid":false,"given":"Jan","family":"Pich","sequence":"first","affiliation":[{"name":"University of Oxford","place":["Oxford, United Kingdom of Great Britain and Northern Ireland"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8716-6091","authenticated-orcid":false,"given":"Rahul","family":"Santhanam","sequence":"additional","affiliation":[{"name":"University of Oxford","place":["Oxford, United Kingdom of Great Britain and Northern Ireland"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2026,4,23]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"S. Aaronson. 2003. Is P Versus NP Formally Independent? Bulletin of EATCS 81 (2003) 109\u2013136."},{"key":"e_1_3_2_3_2","doi-asserted-by":"crossref","unstructured":"M. Ajtai. 1994. The complexity of the pigeonhole principle Combinatorica 14 4 (1994) 417\u2013433.","DOI":"10.1007\/BF01302964"},{"key":"e_1_3_2_4_2","doi-asserted-by":"crossref","unstructured":"A. Akavia O. Goldreich S. Goldwasser D. Moshkovitz. 2006. On basing one-way functions on NP-Hardness. In Symposium on Theory of Computing (STOC) 2006.","DOI":"10.1145\/1132516.1132614"},{"key":"e_1_3_2_5_2","doi-asserted-by":"crossref","unstructured":"I. Alth\u00f6fer. 1994. On sparse approximations to randomized strategies and convex combinations. Linear Algebra and its Applications 199 1 (1994) 339\u2013355.","DOI":"10.1016\/0024-3795(94)90357-3"},{"key":"e_1_3_2_6_2","doi-asserted-by":"crossref","unstructured":"B. Applebaum B. Barak D. Xiao. 2008. On basing lower bounds for learning on worst-case assumptions. Foundations of Computer Science (FOCS). 2008.","DOI":"10.1109\/FOCS.2008.35"},{"key":"e_1_3_2_7_2","unstructured":"N. Arteche E. Khaniki J. Pich R. Santhanam. 2024. From proof complexity to circuit complexity via interactive protocols. International Colloquium on Automata Languages and Programming (ICALP). 2024."},{"key":"e_1_3_2_8_2","unstructured":"A. Atserias. 2006. Distinguishing SAT from polynomial-size circuits through black-box queries. Computational Complexity Conference (CCC). 2006."},{"key":"e_1_3_2_9_2","doi-asserted-by":"crossref","unstructured":"A. Atserias and N. Thapen. 2014. The ordering principle in a fragment of approximate counting. ACM Transactions on Computational Logic 15 4 (2014) 29.","DOI":"10.1145\/2629555"},{"key":"e_1_3_2_10_2","unstructured":"P. Beame and T. Pitassi. 2001. Propositional proof complexity: Past present and future. Current Trends in Theoretical Computer Science Entering the 21st Century (2001) 42\u201370."},{"key":"e_1_3_2_11_2","doi-asserted-by":"crossref","unstructured":"O. Beyersdorff I. Bonacina L. Chew. 2016. Lower bounds: From circuits to QBF proof systems. Innovations in Theoretical Computer Science (ITCS). 2016.","DOI":"10.1145\/2840728.2840740"},{"key":"e_1_3_2_12_2","doi-asserted-by":"crossref","unstructured":"O. Beyersdorff and J. Pich. 2016. Understanding gentzen and frege systems for QBF. LICS. 2016.","DOI":"10.1145\/2933575.2933597"},{"key":"e_1_3_2_13_2","unstructured":"E. Binnendyk M. Carmosino A. Kolokolova R. Ramyaa M. Sabin. 2022. Learning with distributional inverters. Algorithmic Learning Theory (ALT). 2022."},{"key":"e_1_3_2_14_2","unstructured":"A. Bogdanov K. Talwar A. Wan. 2010. Hard instances for satisfiability and quasi-one-way functions. ICS. 2010."},{"key":"e_1_3_2_15_2","doi-asserted-by":"crossref","unstructured":"M. L. Bonet C. Domingo R. Gavald\u00e1 A. Maciel T. Pitassi. 2004. Non-automatizability of bounded-depth Frege proofs. Computational Complexity 13 1-2 (2004) 47\u201368.","DOI":"10.1007\/s00037-004-0183-5"},{"key":"e_1_3_2_16_2","doi-asserted-by":"crossref","unstructured":"M. L. Bonet T. Pitassi R. Raz. 2000. On interpolation and automatization for Frege proof systems. SIAM Journal of Computing 29 6 (2000) 1939\u20131967","DOI":"10.1137\/S0097539798353230"},{"key":"e_1_3_2_17_2","doi-asserted-by":"crossref","unstructured":"M. L. Bonet T. Pitassi R. Raz. 1995. Lower bounds for cutting planes proofs with small coefficients. Symposium on Theory of Computing (STOC). 1995.","DOI":"10.1145\/225058.225275"},{"key":"e_1_3_2_18_2","unstructured":"S. Buss. 1986. Bounded arithmetic. Bibliopolis. 1986."},{"key":"e_1_3_2_19_2","doi-asserted-by":"crossref","unstructured":"P. Beame R. Impagliazzo T. Pitassi. 1993. Exponential lower bounds for the pigeonhole principle. Computational Complexity 3 (1993) 97\u2013140","DOI":"10.1007\/BF01200117"},{"key":"e_1_3_2_20_2","doi-asserted-by":"crossref","unstructured":"A. Bogdanov and Brzuska. 2015. On basing size-verifiable one-way functions on NP-hardness. TCC (1). 2015.","DOI":"10.1007\/978-3-662-46494-6_1"},{"key":"e_1_3_2_21_2","doi-asserted-by":"crossref","unstructured":"A. Bogdanov and L. Trevisan. 2006. On worst-case to average-case reductions for NP problems. SIAM Journal on Computing 36 4 (2006) 1119\u20131159.","DOI":"10.1137\/S0097539705446974"},{"key":"e_1_3_2_22_2","doi-asserted-by":"crossref","unstructured":"S. O. Chan J. R. Lee P. Raghavendra D. Steurer. 2016. Approximate constraint satisfaction requires large LP relaxations. Journal of the ACM 63 4 (2016).","DOI":"10.1145\/2811255"},{"key":"e_1_3_2_23_2","unstructured":"L. Chen C. Jin R. Santhanam R. Williams. 2021. Constructive separations and their consequences. Foundations of Computer Science (FOCS)."},{"key":"e_1_3_2_24_2","unstructured":"A. Cobham. 1965. The intrinsic computational difficulty of functions. Proceedings of the 2nd International Congress of Logic Methodology and Philosophy of Science North Holland.1965 24\u201330."},{"key":"e_1_3_2_25_2","doi-asserted-by":"crossref","unstructured":"S. A. Cook. 1975. Feasibly constructive proofs and the propositional calculus. Symposium on Theory of Computing (STOC). 1975.","DOI":"10.1145\/800116.803756"},{"key":"e_1_3_2_26_2","doi-asserted-by":"crossref","unstructured":"S. A. Cook and N. Thapen. 2006. The strength of replacement in weak arithmetic. ACM Transactions on Computational Logic 7 4 (2006) 749\u2013764.","DOI":"10.1145\/1166109.1166114"},{"key":"e_1_3_2_27_2","doi-asserted-by":"crossref","unstructured":"S. A. Cook and J. Kraj\u00ed\u010dek. 2007. Consequences of the provability of NP \\(\\subseteq\\) P\/poly. Journal of Symbolic Logic 72 (2007) 1353\u20131357.","DOI":"10.2178\/jsl\/1203350791"},{"key":"e_1_3_2_28_2","doi-asserted-by":"crossref","unstructured":"S. A. Cook and R. Reckhow. 1979. The relative efficiency of propositional proof systems. Journal of Symbolic Logic 44 1 (1979) 36\u201350.","DOI":"10.2307\/2273702"},{"key":"e_1_3_2_29_2","unstructured":"B. Davis and R. Robere. 2023. Colourful TFNP and propositional proofs. Computational Complexity Conference (CCC). 2023."},{"key":"e_1_3_2_30_2","unstructured":"S. de Rezende M. G\u00f6\u00f6s R. Robere. 2022. Proofs circuits and communication. SIGACT News Complexity Theory Column. 2022."},{"key":"e_1_3_2_31_2","doi-asserted-by":"crossref","unstructured":"N. Fleming D. Pankratov T. Pitassi R. Robere. 2022. Random \\(O(\\log n)\\) -CNFs are hard for cutting planes. Journal of the ACM 69 3 (2022).","DOI":"10.1145\/3486680"},{"key":"e_1_3_2_32_2","doi-asserted-by":"crossref","unstructured":"J. Grochow and T. Pitassi. 2018. Circuit complexity proof complexity and polynomial identity testing: The ideal proof system. Journal of the ACM 65 6 (2018) 37:1\u201359.","DOI":"10.1145\/3230742"},{"key":"e_1_3_2_33_2","doi-asserted-by":"crossref","unstructured":"D. Gutfreund R. Shaltiel A. Ta-Shma. 2007. If NP languages are hard in the worst-case then it is easy to find their hard instances. Computational Complexity 16 4 (2007) 412\u2013441.","DOI":"10.1007\/s00037-007-0235-8"},{"key":"e_1_3_2_34_2","doi-asserted-by":"crossref","unstructured":"A. Haken. 1985. The intractability of resolution. Theoretical Computer Science 39 (1985) 297\u2013308.","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_3_2_35_2","doi-asserted-by":"crossref","unstructured":"S. Hirahara. 2018. Non-black-box worst-case to average-case reductions within \\({\\sf NP}\\) . Foundations of Computer Science (FOCS).","DOI":"10.1109\/FOCS.2018.00032"},{"key":"e_1_3_2_36_2","doi-asserted-by":"crossref","unstructured":"P. Hrube\u0161 and P. Pudl\u00e1k. 2017. Random formulas monotone circuits and interpolation. Foundations of Computer Science (FOCS).","DOI":"10.1109\/FOCS.2017.20"},{"key":"e_1_3_2_37_2","unstructured":"R. Impagliazzo. 1995. A personal view of average-case complexity. Structure in Complexity Theory (SCT)."},{"key":"e_1_3_2_38_2","unstructured":"R. Impagliazzo and A. Wigderson. 1997. P=BPP unless E has sub-exponential circuits: Derandomizing the XOR lemma. Symposium on Theory of Computing (STOC)."},{"key":"e_1_3_2_39_2","doi-asserted-by":"crossref","unstructured":"E. Je\u0159\u00e1bek. 2004. Dual weak pigeonhole principle boolean complexity and derandomization. Annals of Pure and Applied Logic 129 (2004) 1\u201337.","DOI":"10.1016\/j.apal.2003.12.003"},{"key":"e_1_3_2_40_2","unstructured":"E. Je\u0159\u00e1bek. 2005. Weak pigeonhole principle and randomized computation. Ph.D. Thesis Charles University in Prague"},{"key":"e_1_3_2_41_2","doi-asserted-by":"crossref","unstructured":"E. Je\u0159\u00e1bek. 2007. Approximate counting in bounded arithmetic. Journal of Symbolic Logic 72 (2007) 959\u2013993.","DOI":"10.2178\/jsl\/1191333850"},{"key":"e_1_3_2_42_2","doi-asserted-by":"crossref","unstructured":"V. Kabanets. 2001. Easiness assumptions and hardness tests: Trading time for zero error. Journal of Computer and System Sciences 63 2 (2001) 236\u2013252.","DOI":"10.1006\/jcss.2001.1763"},{"key":"e_1_3_2_43_2","doi-asserted-by":"crossref","unstructured":"R. Kannan. 1982. Circuit-size lower bounds and non-reducibility to sparse sets. Information and Control 55 (1982) 40\u201356","DOI":"10.1016\/S0019-9958(82)90382-5"},{"key":"e_1_3_2_44_2","doi-asserted-by":"crossref","unstructured":"P. Kothari R. Meka and P. Raghavendra. 2017. Approximating rectangles by juntas and weakly-exponential lower bounds for LP relaxations of CSPs. Symposium on Theory of Computing (STOC).","DOI":"10.1145\/3055399.3055438"},{"key":"e_1_3_2_45_2","doi-asserted-by":"crossref","unstructured":"J. Kraj\u00ed\u010dek. 1995. Bounded arithmetic propositional logic and complexity theory. Cambridge University Press.","DOI":"10.1017\/CBO9780511529948"},{"key":"e_1_3_2_46_2","doi-asserted-by":"crossref","unstructured":"J. Kraj\u00ed\u010dek. 1997. Interpolation theorems lower bounds for proof systems and independence results for bounded arithmetic. Journal of Symbolic Logic 66 2 (1997) 457\u2013486.","DOI":"10.2307\/2275541"},{"key":"e_1_3_2_47_2","doi-asserted-by":"crossref","unstructured":"J. Kraj\u00ed\u010dek. 2001. On the weak pigeonhole principle. Fundamenta Mathematicae 170 1-3 (2001) 123\u2013140.","DOI":"10.4064\/fm170-1-8"},{"key":"e_1_3_2_48_2","doi-asserted-by":"crossref","unstructured":"J. Kraj\u00ed\u010dek. 2011. Forcing with random variables and proof complexity. Cambridge University Press.","DOI":"10.1017\/CBO9781139107211"},{"key":"e_1_3_2_49_2","doi-asserted-by":"crossref","unstructured":"J. Kraj\u00ed\u010dek. 2019. Proof complexity. Cambridge University Press.","DOI":"10.1017\/9781108242066"},{"key":"e_1_3_2_50_2","doi-asserted-by":"crossref","unstructured":"J. Kraj\u00ed\u010dek P. Pudl\u00e1k G. Takeuti. 1991. Bounded arithmetic and the polynomial hierarchy. Annals of Pure and Applied Logic 52 (1991) 143\u2013153.","DOI":"10.1016\/0168-0072(91)90043-L"},{"key":"e_1_3_2_51_2","doi-asserted-by":"crossref","unstructured":"J. Kraj\u00ed\u010dek P. Pudl\u00e1k A. Woods. 1995. An exponential lower bound to the size of bounded depth frege proofs of the pigeonhole principle. Random Structures and Algorithms 7 1 (1995) 15\u201340.","DOI":"10.1002\/rsa.3240070103"},{"key":"e_1_3_2_52_2","doi-asserted-by":"crossref","unstructured":"J. R. Lee P. Raghavendra D. Steurer. 2015. Lower bounds on the size of semidefinite programming relaxations. Symposium on Theory of Computing (STOC).","DOI":"10.1145\/2746539.2746599"},{"key":"e_1_3_2_53_2","doi-asserted-by":"crossref","unstructured":"F. Li I. Tzameret Z. Wang. 2018. Characterizing propositional proofs as noncommutative formulas. SIAM Journal on Computing 47 4 (2018) 1424\u20131462.","DOI":"10.1137\/16M1107632"},{"key":"e_1_3_2_54_2","doi-asserted-by":"crossref","unstructured":"R. J. Lipton Young N. E. 1994. Simple strategies for large zero-sum games with applications to complexity theory. Symposium on Theory of Computing (STOC)","DOI":"10.1145\/195058.195447"},{"key":"e_1_3_2_55_2","unstructured":"Y. Liu and R. Pass. 2022. On one-way functions from NP-complete problems. Computational Complexity Conference (CCC)"},{"key":"e_1_3_2_56_2","doi-asserted-by":"crossref","unstructured":"M. M\u00fcller and J. Pich. 2019. Feasibly constructive proofs of succinct weak circuit lower bounds. Annals of Pure and Applied Logic.","DOI":"10.1016\/j.apal.2019.102735"},{"key":"e_1_3_2_57_2","doi-asserted-by":"crossref","unstructured":"I. Newman. 1991. Private vs common random bits in communication complexity. Information Processing Letters 39 (1991) 67\u201371.","DOI":"10.1016\/0020-0190(91)90157-D"},{"key":"e_1_3_2_58_2","doi-asserted-by":"crossref","unstructured":"J. Pich. 2015. Circuit lower bounds in bounded arithmetics. Annals of Pure and Applied Logic 166 1 (2015) 29\u201345.","DOI":"10.1016\/j.apal.2014.08.004"},{"key":"e_1_3_2_59_2","unstructured":"J. Pich and R. Santhanam. 2021. Learning algorithms versus automatability of Frege systems arXiv."},{"key":"e_1_3_2_60_2","doi-asserted-by":"crossref","unstructured":"J. Pich and R. Santhanam. 2019. Why are proof complexity lower bounds hard?. Foundations of Computer Science (FOCS).","DOI":"10.1109\/FOCS.2019.00080"},{"key":"e_1_3_2_61_2","doi-asserted-by":"crossref","unstructured":"T. Pitassi and I. Tzameret. 2016. Algebraic proof complexity: progress frontiers and challenges. ACM SIGLOG News 3 3 (2016) 21\u201343.","DOI":"10.1145\/2984450.2984455"},{"key":"e_1_3_2_62_2","doi-asserted-by":"crossref","unstructured":"Pudl\u00e1k P.; The canonical pairs of bounded depth Frege systems; Annals of Pure and Applied Logic 172(2) 2021.","DOI":"10.1016\/j.apal.2020.102892"},{"key":"e_1_3_2_63_2","doi-asserted-by":"crossref","unstructured":"P. Pudl\u00e1k. 1997. Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic 62 3 (1997).","DOI":"10.2307\/2275583"},{"key":"e_1_3_2_64_2","doi-asserted-by":"crossref","unstructured":"A. A. Razborov. 1995. Bounded arithmetic and lower bounds in boolean complexity. Feasible Mathematics II (1995) 344\u2013386.","DOI":"10.1007\/978-1-4612-2566-9_12"},{"key":"e_1_3_2_65_2","doi-asserted-by":"crossref","unstructured":"A. A. Razborov. 1995. Unprovability of lower bounds on the circuit size in certain fragments of bounded arithmetic Izvestiya of the Russian Academy of Science 59 (1995) 201\u2013224.","DOI":"10.1070\/IM1995v059n01ABEH000009"},{"key":"e_1_3_2_66_2","doi-asserted-by":"crossref","unstructured":"A. A. Razborov. 2015. Pseudorandom generators hard for k-DNF resolution and polynomial calculus. Annals of Mathematics 181 2 (2015) 415\u2013472.","DOI":"10.4007\/annals.2015.181.2.1"},{"key":"e_1_3_2_67_2","unstructured":"R. Santhanam. 2020. Pseudorandomness and the minimum circuit size problem. Innovations in Theoretical Computer Science (ITCS)"},{"key":"e_1_3_2_68_2","doi-asserted-by":"crossref","unstructured":"R. Santhanam and I. Tzameret. 2021. Iterated lower bound formulas: A diagonalization-based approach to proof complexity. Symposium on Theory of Computing (STOC).","DOI":"10.1145\/3406325.3451010"},{"key":"e_1_3_2_69_2","doi-asserted-by":"crossref","unstructured":"R. Williams. 2011. Non-uniform ACC circuit lower bounds. Computational Complexity Conference (CCC).","DOI":"10.1109\/CCC.2011.36"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3801091","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,23]],"date-time":"2026-04-23T16:12:55Z","timestamp":1776960775000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3801091"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,4,23]]},"references-count":68,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,4,30]]}},"alternative-id":["10.1145\/3801091"],"URL":"https:\/\/doi.org\/10.1145\/3801091","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,4,23]]},"assertion":[{"value":"2024-07-19","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-12-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-23","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}