{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T06:47:51Z","timestamp":1765608471165,"version":"3.32.0"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2014,11,9]],"date-time":"2014-11-09T00:00:00Z","timestamp":1415491200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,11,9]],"date-time":"2014-11-09T00:00:00Z","timestamp":1415491200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Axiomathes"],"published-print":{"date-parts":[[2015,3]]},"DOI":"10.1007\/s10516-014-9252-9","type":"journal-article","created":{"date-parts":[[2014,11,14]],"date-time":"2014-11-14T16:49:13Z","timestamp":1415983753000},"page":"79-91","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["What is a Proof?"],"prefix":"10.1007","volume":"25","author":[{"given":"Reinhard","family":"Kahle","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,11,9]]},"reference":[{"key":"9252_CR2","first-page":"147","volume-title":"The argument of mathematics, volume 30 of logic, epistemology and the unity of science","author":"J Alama","year":"2013","unstructured":"Alama J, Kahle R (2013) Checking proofs. In: Aberdein A, Dove IJ (eds) The argument of mathematics, volume 30 of logic, epistemology and the unity of science. Springer, Berlin, pp 147\u2013170"},{"issue":"7","key":"9252_CR3","first-page":"736","volume":"51","author":"M Aschbacher","year":"2004","unstructured":"Aschbacher M (2004) The status of the classification of the finite simple groups. Not Am Math Soc 51(7):736\u2013740","journal-title":"Not Am Math Soc"},{"key":"9252_CR4","doi-asserted-by":"publisher","first-page":"2401","DOI":"10.1098\/rsta.2005.1655","volume":"363","author":"M Aschbacher","year":"2005","unstructured":"Aschbacher M (2005) Highly complex proofs and implications of such proofs. Philos Trans R Soc A 363:2401\u20132406","journal-title":"Philos Trans R Soc A"},{"key":"9252_CR5","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/s11229-005-4064-5","volume":"153","author":"J Avigad","year":"2006","unstructured":"Avigad J (2006) Mathematical method and proof. Synthese 153:105\u2013149","journal-title":"Synthese"},{"issue":"4","key":"9252_CR1","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/2591012","volume":"57","author":"J Avigad","year":"2014","unstructured":"Avigad J, Harrison J (2014) Formally verified mathematics. Commun ACM 57(4):66\u201375","journal-title":"Commun ACM"},{"issue":"1\u20132","key":"9252_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(98)00304-1","volume":"224","author":"M Baaz","year":"1999","unstructured":"Baaz M (1999) Note on the generalization of calculations. Theor Comput Sci 224(1\u20132):3\u201311","journal-title":"Theor Comput Sci"},{"key":"9252_CR8","first-page":"30","volume-title":"Arithmetic proof theory and computational complexity","author":"M Baaz","year":"1993","unstructured":"Baaz M, Pudl\u00e1k P (1993) Kreisel\u2019s conjecture for $$l\\exists _1$$. In: Clote P, Kraj\u00ed\u010dek J (eds) Arithmetic proof theory and computational complexity. Oxford University Press, Oxford, pp 30\u201349"},{"issue":"4","key":"9252_CR7","doi-asserted-by":"publisher","first-page":"221","DOI":"10.2307\/2305937","volume":"57","author":"N Bourbaki","year":"1950","unstructured":"Bourbaki N (1950) The architecture of mathematics. Am Math Mon 57(4):221\u2013232","journal-title":"Am Math Mon"},{"unstructured":"Dieudonn\u00e9 J (1985) Geschichte der Mathematik,\u00a01700\u20131900. Vieweg, Berlin","key":"9252_CR9"},{"key":"9252_CR10","volume-title":"Proof-theoretical coherence","author":"K Do\u0161en","year":"2004","unstructured":"Do\u0161en K, Petri\u0107 Z (2004) Proof-theoretical coherence. KCL Publications, London"},{"unstructured":"Ganesalingam M, Gowers WT (2013) A fully automatic problem solver with human-style output. CoRR, abs\/1309.4501","key":"9252_CR11"},{"key":"9252_CR12","volume-title":"Henri Poincar\u00e9","author":"J Gray","year":"2013","unstructured":"Gray J (2013) Henri Poincar\u00e9. Princeton University Press, Princeton"},{"doi-asserted-by":"crossref","unstructured":"Hales TC (2014) Mathematics in the age of the Turing machine. In: Downey R (ed) Turing\u2019s legacy: developments from Turing\u2019s ideas in logic, volume 42 of lecture notes in logic. ASL and Cambridge University Press, pp 253\u2013298","key":"9252_CR13","DOI":"10.1017\/CBO9781107338579.008"},{"key":"9252_CR15","volume-title":"An introduction to the theory of numbers","author":"GH Hardy","year":"1960","unstructured":"Hardy GH, Wright EM (1960) An introduction to the theory of numbers, 4th edn. Oxford University Press, Oxford","edition":"4"},{"unstructured":"Hughes B (1987) Mathematical proof: origins and development. In: Grattan-Guinness I (ed) History in mathematics education. Number 21 in Cahiers d\u2019Histoire et de Philosophie des Sciences. Nouvelle S\u00e9rie, pp 65\u201372. Soci\u00e9t\u00e9 Fran\u00e7aise d\u2019Histoire des Sciences et des Techniques. Belin","key":"9252_CR14"},{"unstructured":"Kahle R (2014) Towards the structure of mathematical proof. In: England M et al (eds) Joint proceedings of the MathUI, OpenMath and ThEdu workshops and work in progress track at CICM, vol 1186 of CEUR workshop proceedings","key":"9252_CR16"},{"key":"9252_CR17","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/BF01625836","volume":"27","author":"J Kraj\u00ed\u010dek","year":"1988","unstructured":"Kraj\u00ed\u010dek J, Pudl\u00e1k P (1988) The number of proof lines and the size of proofs in first order logic. Arch Math Log 27:69\u201384","journal-title":"Arch Math Log"},{"key":"9252_CR18","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BF01703261","volume":"2","author":"J Lambek","year":"1968","unstructured":"Lambek J (1968) Deductive systems and categories. I: syntactic calculus and residuated categories. Math Syst Theory 2:287\u2013318","journal-title":"Math Syst Theory"},{"doi-asserted-by":"crossref","unstructured":"Lambek J (1969) Deductive systems and categories II. Standard constructions and closed categories. In: Hilton P (ed) Category theory, homology theory and applications, volume 86 of lecture notes in mathematics, vol 86. Springer, pp 76\u2013122","key":"9252_CR19","DOI":"10.1007\/BFb0079385"},{"issue":"7","key":"9252_CR20","doi-asserted-by":"publisher","first-page":"600","DOI":"10.2307\/2974556","volume":"102","author":"L Lamport","year":"1995","unstructured":"Lamport L (1995) How to write a proof. Am Math Mon 102(7):600\u2013608","journal-title":"Am Math Mon"},{"key":"9252_CR21","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s11784-012-0071-6","volume":"11","author":"L Lamport","year":"2012","unstructured":"Lamport L (2012) How to write a 21st century proof. J Fixed Point Theory Appl 11:43\u201363","journal-title":"J Fixed Point Theory Appl"},{"issue":"3","key":"9252_CR22","doi-asserted-by":"publisher","first-page":"174","DOI":"10.2307\/2975544","volume":"90","author":"U Leron","year":"1983","unstructured":"Leron U (1983) Structuring mathematical proofs. Am Math Mon 90(3):174\u2013185","journal-title":"Am Math Mon"},{"unstructured":"Loomis ES (1968) The Pythagorean proposition. Ann Arbor Michigan, 1968. Reprint of the 2nd edition from 1940. First published in 1927","key":"9252_CR23"},{"key":"9252_CR24","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-94-015-9558-2_8","volume-title":"The growth of mathematical knowledge","author":"P Mancosu","year":"2000","unstructured":"Mancosu P (2000) On mathematical explanation. In: Grosholz E, Breger H (eds) The growth of mathematical knowledge. Kluwer, Netherlands, pp 103\u2013119"},{"key":"9252_CR25","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1023\/A:1010621314372","volume":"20","author":"P Mancosu","year":"2001","unstructured":"Mancosu P (2001) Mathematical explanation: problems and prospects. Topoi 20:97\u2013117","journal-title":"Topoi"},{"doi-asserted-by":"crossref","unstructured":"Necula GC (1997) Proof-carrying code. In: POPL \u201997. ACM Press, pp 106\u2013119","key":"9252_CR26","DOI":"10.1145\/263699.263712"},{"key":"9252_CR27","volume-title":"Natural deduction, a proof-theoretical study","author":"D Prawitz","year":"1965","unstructured":"Prawitz D (1965) Natural deduction, a proof-theoretical study. Almquist and Wiksell, Stockholm"},{"doi-asserted-by":"crossref","unstructured":"Prawitz D (1971) Ideas and results in proof theory. In: Fenstad JE (ed) Proceedings of the Second Scandinavian Logic Symposium. North-Holland, pp 235\u2013307","key":"9252_CR28","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"9252_CR29","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1090\/S1079-6762-96-00003-0","volume":"2","author":"N Robertson","year":"1996","unstructured":"Robertson N, Sanders DP, Seymour PD, Thomas R (1996) A new proof of the four colour theorem. Electron Res Announc Am Math Soc 2:17\u201325","journal-title":"Electron Res Announc Am Math Soc"},{"unstructured":"Scott D (2006) Foreword. In: Wiedijk F (ed) The seventeen provers of the world, volume 3600 of lecture notes in computer science. Springer, pp vii\u2013xii","key":"9252_CR30"},{"key":"9252_CR31","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00354494","volume":"34","author":"M Steiner","year":"1978","unstructured":"Steiner M (1978) Mathematical explanation. Philos Stud 34:133\u2013151","journal-title":"Philos Stud"},{"key":"9252_CR32","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-7643-7304-0_8","volume-title":"Logica Universalis","author":"L Stra\u00dfburger","year":"2005","unstructured":"Stra\u00dfburger L (2005) What is a logic, and what is a proof? In: Beziau J-Y (ed) Logica Universalis. Birkh\u00e4user, Basel, pp 135\u2013145"},{"doi-asserted-by":"crossref","unstructured":"Trybulec A (2006) Mizar. In: Wiedijk F (ed) The seventeen provers of the world, volume 3600 of lecture notes in computer science, vol 3600. Springer, pp 20\u201323","key":"9252_CR33","DOI":"10.1007\/11542384_4"},{"doi-asserted-by":"crossref","unstructured":"Wenzel M (1999) Isar\u2014a generic interpretative approach to readable formal proof documents. In: Bertot Y, Dowek G, Hirschowitz A, Paulin C, Th\u00e9ry L (eds) Theorem proving in higher order logics, volume 1690 of lecture notes in computer science. Springer, pp 167\u2013184","key":"9252_CR34","DOI":"10.1007\/3-540-48256-3_12"},{"unstructured":"Wenzel M (2002) Isabelle\/Isar\u2014a versatile environment for human-readable formal proof documents. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen","key":"9252_CR35"},{"doi-asserted-by":"crossref","unstructured":"Wenzel M, Paulson L (2006) Isabelle\/Isar. In: Wiedijk F (ed) The seventeen provers of the world, volume 3600 of lecture notes in computer science. Springer, pp 41\u201349","key":"9252_CR37","DOI":"10.1007\/11542384_8"},{"doi-asserted-by":"crossref","unstructured":"Wiedijk F (ed) (2006) The seventeen provers of the world, volume 3600 of lecture notes in computer science. Springer","key":"9252_CR36","DOI":"10.1007\/11542384"}],"container-title":["Axiomathes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10516-014-9252-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10516-014-9252-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10516-014-9252-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10516-014-9252-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,3]],"date-time":"2025-01-03T18:56:53Z","timestamp":1735930613000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10516-014-9252-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,11,9]]},"references-count":37,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,3]]}},"alternative-id":["9252"],"URL":"https:\/\/doi.org\/10.1007\/s10516-014-9252-9","relation":{},"ISSN":["1122-1151","1572-8390"],"issn-type":[{"type":"print","value":"1122-1151"},{"type":"electronic","value":"1572-8390"}],"subject":[],"published":{"date-parts":[[2014,11,9]]},"assertion":[{"value":"15 May 2014","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 October 2014","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 November 2014","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}