{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T09:51:51Z","timestamp":1782899511164,"version":"3.54.5"},"reference-count":39,"publisher":"World Scientific Pub Co Pte Ltd","issue":"02","funder":[{"name":"Royal Society University Research Fellowship","award":["URF\\R1\\211106"],"award-info":[{"award-number":["URF\\R1\\211106"]}]},{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\\V048201\\1"],"award-info":[{"award-number":["EP\\V048201\\1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Marie Sk\u0142odovska-Curie","award":["890220"],"award-info":[{"award-number":["890220"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Math. Log."],"published-print":{"date-parts":[[2026,8]]},"abstract":"<jats:p>We connect learning algorithms and algorithms automating proof search in propositional proof systems: for every sufficiently strong, well-behaved propositional proof system P, we prove that the following statements are equivalent,<\/jats:p>\n                  <jats:p>(1) Provable learning.\u00a0P proves efficiently that p-size circuits are learnable by subexponential-size circuits over the uniform distribution with membership queries.<\/jats:p>\n                  <jats:p>(2) Provable automatability.\u00a0P proves efficiently that P is automatable by non-uniform circuits on propositional formulas expressing p-size circuit lower bounds.<\/jats:p>\n                  <jats:p>Here, P is sufficiently strong and well-behaved if I.\u2013III. hold: I. P p-simulates Je\u0159\u00e1bek\u2019s system WF (which strengthens the Extended Frege system EF by a surjective weak pigeonhole principle); II. P satisfies some basic properties of standard proof systems which p-simulate WF ; III. P proves efficiently for some Boolean function h that h is hard on average for circuits of subexponential size. For example, if III. holds for [Formula: see text], then Items 1 and 2 are equivalent for [Formula: see text]. We use the following modified notion of automatability in Item 2, the automating circuits output a P-proof of a given formula (expressing a p-size circuit lower bound for a function f) in non-uniform p-time in the length of a shortest P-proof of a closely related but different formula (expressing an average-case subexponential-size circuit lower bound for the same function f).<\/jats:p>\n                  <jats:p>If there is a function [Formula: see text] which is hard on average for circuits of size [Formula: see text], for each sufficiently big n, then there is an explicit propositional proof system P satisfying properties I.-III., i.e. the equivalence of Items 1 and 2 holds for P.<\/jats:p>","DOI":"10.1142\/s0219061325500023","type":"journal-article","created":{"date-parts":[[2024,11,15]],"date-time":"2024-11-15T09:56:54Z","timestamp":1731664614000},"source":"Crossref","is-referenced-by-count":0,"title":["Learning algorithms versus automatability of Frege systems"],"prefix":"10.1142","volume":"26","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2731-1330","authenticated-orcid":false,"given":"J\u00e1n","family":"Pich","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Oxford, Wolfson building, Parks road, OX1 3QD, Oxford, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8716-6091","authenticated-orcid":false,"given":"Rahul","family":"Santhanam","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Oxford, Wolfson building, Parks road, OX1 3QD, Oxford, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"219","published-online":{"date-parts":[[2024,12,31]]},"reference":[{"key":"S0219061325500023BIB001","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2004.36"},{"key":"S0219061325500023BIB002","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2008.35"},{"key":"S0219061325500023BIB003","doi-asserted-by":"publisher","DOI":"10.1109\/FOCS.2019.00038"},{"key":"S0219061325500023BIB004","first-page":"90","volume-title":"Proc. 33rd Int. Conf. Algorithmic Learning Theory","author":"Binnendyk E.","year":"2022"},{"key":"S0219061325500023BIB005","doi-asserted-by":"publisher","DOI":"10.1007\/s00037-004-0183-5"},{"key":"S0219061325500023BIB006","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539798353230"},{"key":"S0219061325500023BIB007","volume-title":"Bounded Arithmetic","author":"Buss S.","year":"1986"},{"key":"S0219061325500023BIB008","first-page":"1","volume-title":"Proc. 31st Conf. Computational Complexity","author":"Carmosino M.","year":"2016"},{"key":"S0219061325500023BIB009","first-page":"24","volume-title":"Proc. 2nd Int. Congress of Logic, Methodology and Philosophy of Science","author":"Cobham A.","year":"1965"},{"key":"S0219061325500023BIB010","first-page":"83","volume-title":"Proc. seventh annual ACM Symposium on Theory of computing","author":"Cook S. A.","year":"1975"},{"key":"S0219061325500023BIB011","doi-asserted-by":"publisher","DOI":"10.1145\/1183278.1183283"},{"key":"S0219061325500023BIB012","doi-asserted-by":"publisher","DOI":"10.1145\/3406325.3451080"},{"key":"S0219061325500023BIB013","first-page":"1","volume-title":"39th Computational Complexity Conference","author":"Garl\u00edk M.","year":"2024"},{"key":"S0219061325500023BIB014","doi-asserted-by":"publisher","DOI":"10.1145\/3357713.3384248"},{"key":"S0219061325500023BIB015","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2003.12.003"},{"key":"S0219061325500023BIB016","unstructured":"E. Je\u0159\u00e1bek,\n                      Weak Pigeonhole Principle and Randomized Computation\n                      , Ph.D. thesis, Charles University in Prague (1999)."},{"key":"S0219061325500023BIB017","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1191333850"},{"key":"S0219061325500023BIB018","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511529948"},{"key":"S0219061325500023BIB019","doi-asserted-by":"publisher","DOI":"10.2307\/2275541"},{"key":"S0219061325500023BIB020","doi-asserted-by":"publisher","DOI":"10.4064\/fm170-1-8"},{"key":"S0219061325500023BIB021","volume-title":"Forcing with Random Variables and Proof Complexity","author":"Kraj\u00ed\u010dek J.","year":"2011"},{"key":"S0219061325500023BIB022","doi-asserted-by":"publisher","DOI":"10.1017\/9781108242066"},{"key":"S0219061325500023BIB023","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2674"},{"key":"S0219061325500023BIB024","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90043-L"},{"key":"S0219061325500023BIB025","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2019.102735"},{"key":"S0219061325500023BIB026","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(05)80043-1"},{"key":"S0219061325500023BIB027","first-page":"1","volume-title":"Proc. 32nd Computational Complexity Conference","author":"Oliveira I. C.","year":"2017"},{"key":"S0219061325500023BIB028","doi-asserted-by":"publisher","DOI":"10.2307\/2274618"},{"key":"S0219061325500023BIB029","unstructured":"J. Pich, Learning algorithms from circuit lower bounds, preprint (2020)."},{"key":"S0219061325500023BIB030","first-page":"370","volume-title":"Innovations in Computer Science","author":"Pitassi T.","year":"2010"},{"key":"S0219061325500023BIB031","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1016\/S0049-237X(08)70462-2","volume-title":"Logic Colloquium 84","volume":"120","author":"Pudl\u00e1k P.","year":"1986"},{"key":"S0219061325500023BIB032","doi-asserted-by":"crossref","unstructured":"A. A. Razborov, On provably disjoint NP pairs, Technical Report RS-94-36, BRICS (1994).","DOI":"10.7146\/brics.v1i36.21607"},{"key":"S0219061325500023BIB033","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2566-9_12"},{"key":"S0219061325500023BIB034","first-page":"201","volume":"59","author":"Razborov A. A.","year":"1995","journal-title":"Izv. Ross. Akad. Nauk Ser. Mat."},{"key":"S0219061325500023BIB035","doi-asserted-by":"publisher","DOI":"10.4007\/annals.2015.181.2.1"},{"key":"S0219061325500023BIB036","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1997.1494"},{"key":"S0219061325500023BIB037","first-page":"1","volume-title":"11th Innovations in Theoretical Computer Science Conference","author":"Santhanam R.","year":"2020"},{"key":"S0219061325500023BIB038","doi-asserted-by":"publisher","DOI":"10.1145\/1968.1972"},{"key":"S0219061325500023BIB039","doi-asserted-by":"publisher","DOI":"10.1109\/CCC.2011.36"}],"container-title":["Journal of Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.worldscientific.com\/doi\/pdf\/10.1142\/S0219061325500023","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T09:39:28Z","timestamp":1782898768000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.worldscientific.com\/doi\/10.1142\/S0219061325500023"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,31]]},"references-count":39,"journal-issue":{"issue":"02","published-print":{"date-parts":[[2026,8]]}},"alternative-id":["10.1142\/S0219061325500023"],"URL":"https:\/\/doi.org\/10.1142\/s0219061325500023","relation":{},"ISSN":["0219-0613","1793-6691"],"issn-type":[{"value":"0219-0613","type":"print"},{"value":"1793-6691","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,12,31]]},"article-number":"2550002"}}