{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,13]],"date-time":"2025-05-13T23:13:44Z","timestamp":1747178024238,"version":"3.40.5"},"reference-count":41,"publisher":"Informa UK Limited","issue":"2","license":[{"start":{"date-parts":[[2021,10,21]],"date-time":"2021-10-21T00:00:00Z","timestamp":1634774400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":["www.tandfonline.com"],"crossmark-restriction":true},"short-container-title":["Experimental Mathematics"],"published-print":{"date-parts":[[2022,4,3]]},"DOI":"10.1080\/10586458.2021.1980465","type":"journal-article","created":{"date-parts":[[2021,10,21]],"date-time":"2021-10-21T17:20:50Z","timestamp":1634836850000},"page":"401-412","update-policy":"https:\/\/doi.org\/10.1080\/tandf_crossmark_01","source":"Crossref","is-referenced-by-count":1,"title":["Irrationality and Transcendence Criteria for Infinite Series in Isabelle\/HOL"],"prefix":"10.1080","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8886-5281","authenticated-orcid":false,"given":"Angeliki","family":"Koutsoukou-Argyraki","sequence":"first","affiliation":[{"name":"Computer Laboratory, University of Cambridge, 15 JJ Thomson Avenue, Cambridge CB3 0FD, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9886-9542","authenticated-orcid":false,"given":"Wenda","family":"Li","sequence":"additional","affiliation":[{"name":"Computer Laboratory, University of Cambridge, 15 JJ Thomson Avenue, Cambridge CB3 0FD, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0288-4279","authenticated-orcid":false,"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[{"name":"Computer Laboratory, University of Cambridge, 15 JJ Thomson Avenue, Cambridge CB3 0FD, UK"}]}],"member":"301","published-online":{"date-parts":[[2021,10,21]]},"reference":[{"key":"CIT0001","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-7288-0"},{"issue":"1","key":"CIT0002","first-page":"101","volume":"9","author":"Blanchette J. C.","year":"2016","journal-title":"J. Formaliz. Reason"},{"key":"CIT0003","unstructured":"Bordg, A., Paulson C., L. and Li, W. Grothendieck\u2019s Schemes in Algebraic Geometry, Archive of Formal Proofs (2021), formal proof development, Available at: https:\/\/isa-afp.org\/entries\/Grothendieck_Schemes.html."},{"key":"CIT0004","doi-asserted-by":"crossref","unstructured":"Bordg, A., Paulson C., L. and Li, W. (2021). Simple Type Theory is not too Simple: Grothendieck\u2019s Schemes without Dependent Types, arXiv:2104.09366.","DOI":"10.1080\/10586458.2022.2062073"},{"key":"CIT0005","first-page":"238","volume-title":"Automated Deduction \u2013 CADE 12, LNAI","volume":"814","author":"Boyer R.","year":"1994"},{"first-page":"299","volume-title":"CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs","author":"Buzzard K.","key":"CIT0006"},{"volume-title":"Proceedings of Interactive Theorem Proving (ITP)","year":"2019","author":"Dahmen S. R.","key":"CIT0007"},{"key":"CIT0008","doi-asserted-by":"publisher","DOI":"10.1145\/3326229.3326240"},{"key":"CIT0009","unstructured":"Eberl, M. Elementary Facts About the Distribution of Primes, Archive of Formal Proofs (2019), formal proof development. Available at: https:\/\/www.isa-afp.org\/entries\/Prime_Distribution_Elementary.html."},{"key":"CIT0010","unstructured":"Eberl, M., Paulson, L.C. The Prime Number Theorem, Archive of Formal Proofs (2018), formal proof development. Available at: https:\/\/www.isa-afp.org\/entries\/Prime_Number_Theorem.html."},{"key":"CIT0011","first-page":"93","volume":"4","author":"Erd\u0151s P.","year":"1958","journal-title":"Enseignment Math"},{"key":"CIT0012","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00541025","volume":"10","author":"Erd\u0151s P.","year":"1975","journal-title":"J. Math. Sci"},{"key":"CIT0013","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1974.55.85"},{"key":"CIT0014","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1971.36.635"},{"issue":"11","key":"CIT0015","first-page":"1382","volume":"55","author":"Gonthier G.","year":"2008","journal-title":"Not. Am. Math. Soc"},{"key":"CIT0016","doi-asserted-by":"publisher","DOI":"10.1016\/j.jfa.2019.02.021"},{"key":"CIT0017","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-0346-0422-2_4"},{"key":"CIT0018","doi-asserted-by":"publisher","DOI":"10.4007\/annals.2005.162.1065"},{"key":"CIT0019","doi-asserted-by":"publisher","DOI":"10.1017\/fmp.2017.1"},{"key":"CIT0020","doi-asserted-by":"publisher","DOI":"10.1006\/jnth.1993.1010"},{"key":"CIT0021","first-page":"177","volume":"46","author":"Han\u010dl J.","year":"1996","journal-title":"Math. Slov"},{"key":"CIT0022","first-page":"149","volume":"56","author":"Han\u010dl J.","year":"2001","journal-title":"Le Matematiche"},{"key":"CIT0023","first-page":"225","volume":"107","author":"Han\u010dl J.","year":"2002","journal-title":"Rend. Sem. Mat. Univ. Padova"},{"key":"CIT0024","doi-asserted-by":"publisher","DOI":"10.1216\/rmjm\/1181069744"},{"key":"CIT0025","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_21"},{"key":"CIT0026","unstructured":"Jutting, L.S. van Benthem. Checking Landau\u2019s \u201cGrundlagen\u201d in the AUTOMATH system. PhD thesis, Eindhoven University of Technology (1977). 10.6100\/IR23183."},{"key":"CIT0027","doi-asserted-by":"publisher","DOI":"10.1365\/s13291-020-00221-1"},{"key":"CIT0028","unstructured":"Koutsoukou-Argyraki, A., Li, W. Irrational rapidly convergent series, Archive of Formal Proofs (2018), formal proof development. Available at: https:\/\/www.isa-afp.org\/entries\/Irrationality_J_Hancl.html."},{"key":"CIT0029","unstructured":"Koutsoukou-Argyraki, A., Li, W. The transcendence of certain infinite series, Archive of Formal Proofs (2019), formal proof development, Available at: https:\/\/www.isa-afp.org\/entries\/Transcendence_Series_Hancl_Rucki.html."},{"key":"CIT0030","unstructured":"Koutsoukou-Argyraki, A., Li, W. Irrationality Criteria for Series by Erd\u0151s and Straus, Archive of Formal Proofs (2020), formal proof development. Available at: https:\/\/www.isa-afp.org\/entries\/Irrational_Series_Erdos_Straus.html."},{"key":"CIT0031","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0081107"},{"key":"CIT0032","volume-title":"Lecture Notes in Computer Science","volume":"2283","author":"Nipkow T.","year":"2002"},{"volume-title":"Mahler Functions and Transcendence, Lecture Notes in Mathematics 1631","year":"1996","author":"Nishioka K.","key":"CIT0033"},{"key":"CIT0034","doi-asserted-by":"publisher","DOI":"10.1216\/rmjm\/1021477261"},{"key":"CIT0035","doi-asserted-by":"publisher","DOI":"10.1006\/jnth.2001.2672"},{"key":"CIT0036","doi-asserted-by":"publisher","DOI":"10.1007\/BF00248324"},{"key":"CIT0037","unstructured":"Paulson, L. C. ALEXANDRIA: Large-scale formal proof for the working mathematician, project description, (12 Nov. 2018). Available at: http:\/\/www.cl.cam.ac.uk\/lp15\/Grants\/Alexandria\/."},{"issue":"3","key":"CIT0038","first-page":"1","volume":"2","author":"Roth K. F.","year":"1955","journal-title":"Mathematica"},{"key":"CIT0039","first-page":"3","volume":"29","author":"S\u00e1ndor J.","year":"1994","journal-title":"Studia Univ. Babe\u015f-Bolyai Math"},{"key":"CIT0040","unstructured":"Wiedijk, F. The De Bruijn Factor, Technical report. Nijmegen, Netherlands: Department of Computer Science Nijmegen University. Available at: https:\/\/www.cs.ru.nl\/freek\/factor\/factor.pdf."},{"key":"CIT0041","unstructured":"Wiedijk, F. The De Bruijn Factor (webpage). Available at: http:\/\/www.cs.ru.nl\/freek\/factor\/."}],"container-title":["Experimental Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.tandfonline.com\/doi\/pdf\/10.1080\/10586458.2021.1980465","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,8]],"date-time":"2022-08-08T16:12:38Z","timestamp":1659975158000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.tandfonline.com\/doi\/full\/10.1080\/10586458.2021.1980465"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,21]]},"references-count":41,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,4,3]]}},"alternative-id":["10.1080\/10586458.2021.1980465"],"URL":"https:\/\/doi.org\/10.1080\/10586458.2021.1980465","relation":{},"ISSN":["1058-6458","1944-950X"],"issn-type":[{"type":"print","value":"1058-6458"},{"type":"electronic","value":"1944-950X"}],"subject":[],"published":{"date-parts":[[2021,10,21]]},"assertion":[{"value":"The publishing and review policy for this title is described in its Aims & Scope.","order":1,"name":"peerreview_statement","label":"Peer Review Statement"},{"value":"http:\/\/www.tandfonline.com\/action\/journalInformation?show=aimsScope&journalCode=uexm20","URL":"http:\/\/www.tandfonline.com\/action\/journalInformation?show=aimsScope&journalCode=uexm20","order":2,"name":"aims_and_scope_url","label":"Aim & Scope"},{"value":"2021-10-21","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}