{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,18]],"date-time":"2026-09-18T08:03:20Z","timestamp":1789718600098,"version":"4.0.1"},"reference-count":47,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2026,9,18]],"date-time":"2026-09-18T00:00:00Z","timestamp":1789689600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["The Review of Symbolic Logic"],"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>This paper investigates the question: what is a formal logical proof (in general\u2014as opposed to: what is a formal proof in this or that specific proof system)? I begin by setting out a core conception of formal proof and substantiating its designation as \u2018core\u2019. The heart of this conception is that there must be an effective or mechanical procedure for checking the correctness of a purported proof. I then consider a proposed strengthening of this conception\u2014one that has become standard in the literature on propositional proof complexity\u2014according to which the proof-checking procedure must be able to be carried out in polynomial time. I discuss a variety of arguments in favour of the strengthened conception\u2014and reject them all. My conclusion is that, when it comes to analysing the very idea of formal logical proof, we have no good reason to move to the strengthened conception and should stick with the core conception.<\/jats:p>","DOI":"10.1017\/s1755020326101300","type":"journal-article","created":{"date-parts":[[2026,9,18]],"date-time":"2026-09-18T07:23:37Z","timestamp":1789716217000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["THE PROOF IS IN THE CHECKING"],"prefix":"10.1017","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2632-1032","authenticated-orcid":false,"given":"NICHOLAS J. J.","family":"SMITH","sequence":"first","affiliation":[{"id":[{"id":"https:\/\/ror.org\/0384j8v12","id-type":"ROR","asserted-by":"publisher"}],"name":"THE UNIVERSITY OF SYDNEY"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2026,9,18]]},"reference":[{"key":"S1755020326101300_r18","unstructured":"[18] Hartmanis, J. (1989). G\u00f6del, von Neumann and the P=?NP problem. Technical Report TR 89-994, Department of Computer Science, Cornell University."},{"key":"S1755020326101300_r40","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1203350879"},{"key":"S1755020326101300_r20","first-page":"369","volume-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879\u20131931","author":"Hilbert","year":"1925"},{"key":"S1755020326101300_r32","first-page":"235","volume-title":"Proceedings of the Second Scandinavian Logic Symposium","author":"Prawitz","year":"1971"},{"key":"S1755020326101300_r11","doi-asserted-by":"publisher","DOI":"10.1525\/9780520312364"},{"key":"S1755020326101300_r17","doi-asserted-by":"publisher","DOI":"10.1093\/mind\/XXXVIII.149.1"},{"key":"S1755020326101300_r13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-6597-3_3"},{"key":"S1755020326101300_r9","doi-asserted-by":"publisher","DOI":"10.2307\/2273702"},{"key":"S1755020326101300_r1","unstructured":"[1] Aaronson, S. (2011). Why philosophers should care about computational complexity. Technical Report 108 (Revision 2), Electronic Colloquium on Computational Complexity."},{"key":"S1755020326101300_r25","first-page":"198","volume-title":"Logic, Methodology and Philosophy of Science: Proceedings of the 1960 International Congress","author":"Kreisel","year":"1962"},{"key":"S1755020326101300_r30","doi-asserted-by":"publisher","DOI":"10.1109\/85.397057"},{"key":"S1755020326101300_r34","doi-asserted-by":"publisher","DOI":"10.1007\/BF00660889"},{"key":"S1755020326101300_r42","volume-title":"Introduction to the Theory of Computation","author":"Sipser","year":"2013"},{"key":"S1755020326101300_r4","first-page":"42","volume-title":"Current Trends in Theoretical Computer Science: Entering the 21st Century","author":"Beame","year":"2001"},{"key":"S1755020326101300_r24","doi-asserted-by":"publisher","DOI":"10.1093\/bjps\/IX.34.135"},{"key":"S1755020326101300_r12","volume-title":"Basic Laws of Arithmetic: Derived Using Concept-Script","author":"Frege","year":"2013"},{"key":"S1755020326101300_r6","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198751410.001.0001"},{"key":"S1755020326101300_r3","doi-asserted-by":"publisher","DOI":"10.1090\/pcms\/010\/07"},{"key":"S1755020326101300_r5","doi-asserted-by":"publisher","DOI":"10.1007\/s11098-012-9903-x"},{"key":"S1755020326101300_r26","doi-asserted-by":"publisher","DOI":"10.2307\/2270324"},{"key":"S1755020326101300_r31","doi-asserted-by":"publisher","DOI":"10.2307\/2269958"},{"key":"S1755020326101300_r21","first-page":"464","volume-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879\u20131931","author":"Hilbert","year":"1927"},{"key":"S1755020326101300_r41","first-page":"603","volume-title":"STOC \u201992: Proceedings of the Twenty-Fourth Annual ACM Symposium on Theory of Computing","author":"Sipser","year":"1992"},{"key":"S1755020326101300_r36","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-018-9785-9"},{"key":"S1755020326101300_r38","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46011-X_8"},{"key":"S1755020326101300_r43","volume-title":"Logic: The Laws of Truth","author":"Smith","year":"2012"},{"key":"S1755020326101300_r44","volume-title":"Natural Logic","author":"Tennant","year":"1990"},{"key":"S1755020326101300_r10","first-page":"1","volume-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879\u20131931","author":"Frege","year":"1879"},{"key":"S1755020326101300_r33","first-page":"225","volume-title":"Logic, Methodology and Philosophy of Science IV: Proceedings of the Fourth International Congress for Logic, Methodology and Philosophy of Science, Bucharest, 1971","author":"Prawitz","year":"1973"},{"key":"S1755020326101300_r14","first-page":"68","volume-title":"The Collected Papers of Gerhard Gentzen","author":"Gentzen","year":"1969"},{"key":"S1755020326101300_r8","first-page":"1","volume-title":"Handbook of Proof Theory","author":"Buss","year":"1998"},{"key":"S1755020326101300_r37","first-page":"547","volume-title":"Handbook of Proof Theory","author":"Pudl\u00e1k","year":"1998"},{"key":"S1755020326101300_r46","volume-title":"Principia Mathematica","volume":"I","author":"Whitehead","year":"1910"},{"key":"S1755020326101300_r16","first-page":"41","volume-title":"The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions","author":"G\u00f6del","year":"1965"},{"key":"S1755020326101300_r22","doi-asserted-by":"publisher","DOI":"10.4324\/9780203290644"},{"key":"S1755020326101300_r47","volume-title":"The Stanford Encyclopedia of Philosophy","author":"Zach","year":"2023"},{"key":"S1755020326101300_r45","doi-asserted-by":"publisher","DOI":"10.2307\/421131"},{"key":"S1755020326101300_r15","first-page":"596","volume-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879\u20131931","author":"G\u00f6del","year":"1931"},{"key":"S1755020326101300_r27","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/S0049-237X(08)70845-0","article-title":"A survey of proof theory II","volume":"63","author":"Kreisel","year":"1971","journal-title":"Studies in Logic and the Foundations of Mathematics"},{"key":"S1755020326101300_r23","volume-title":"Mathematical Logic","author":"Kleene","year":"1967"},{"key":"S1755020326101300_r2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804090"},{"key":"S1755020326101300_r39","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60178-3_78"},{"key":"S1755020326101300_r7","volume-title":"Philosophical Logic","author":"Burgess","year":"2009"},{"key":"S1755020326101300_r35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11041-7_3"},{"key":"S1755020326101300_r19","first-page":"129","volume-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879\u20131931","author":"Hilbert","year":"1904"},{"key":"S1755020326101300_r28","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/8009.003.0005"},{"key":"S1755020326101300_r29","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198514763.003.0006"}],"container-title":["The Review of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1755020326101300","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,18]],"date-time":"2026-09-18T07:23:44Z","timestamp":1789716224000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1755020326101300\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,9,18]]},"references-count":47,"alternative-id":["S1755020326101300"],"URL":"https:\/\/doi.org\/10.1017\/s1755020326101300","relation":{},"ISSN":["1755-0203","1755-0211"],"issn-type":[{"value":"1755-0203","type":"print"},{"value":"1755-0211","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,9,18]]},"assertion":[{"value":"\u00a9 The Author(s), 2026. Published by Cambridge University Press on behalf of The Association for Symbolic Logic","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution-NonCommercial-NoDerivatives licence (https:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/), which permits non-commercial re-use, distribution, and reproduction in any medium, provided the original work is unaltered and is properly cited. The written permission of Cambridge University Press must be obtained for commercial re-use or in order to create a derivative work.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}