{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T19:07:57Z","timestamp":1774984077013,"version":"3.50.1"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2017,2,8]],"date-time":"2017-02-08T00:00:00Z","timestamp":1486512000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,2,8]],"date-time":"2017-02-08T00:00:00Z","timestamp":1486512000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000121","name":"Division of Mathematical Sciences","doi-asserted-by":"publisher","award":["DMS-1068829"],"award-info":[{"award-number":["DMS-1068829"]}],"id":[{"id":"10.13039\/100000121","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-12-1-0370"],"award-info":[{"award-number":["FA9550-12-1-0370"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"crossref","award":["FA9550-15-1-0053"],"award-info":[{"award-number":["FA9550-15-1-0053"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["Ni 491\/15-1"],"award-info":[{"award-number":["Ni 491\/15-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["Ni 491\/16-1"],"award-info":[{"award-number":["Ni 491\/16-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,12]]},"DOI":"10.1007\/s10817-017-9404-x","type":"journal-article","created":{"date-parts":[[2017,2,8]],"date-time":"2017-02-08T08:55:40Z","timestamp":1486544140000},"page":"389-423","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["A Formally Verified Proof of the Central Limit Theorem"],"prefix":"10.1007","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1275-315X","authenticated-orcid":false,"given":"Jeremy","family":"Avigad","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0869-9250","authenticated-orcid":false,"given":"Johannes","family":"H\u00f6lzl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luke","family":"Serafin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,2,8]]},"reference":[{"key":"9404_CR1","unstructured":"Avigad, J., H\u00f6lzl, J., Serafin, L.: A formally verified proof of the central limit theorem (preliminary announcement) CoRR (2014). http:\/\/arxiv.org\/abs\/1405.7012v1"},{"key":"9404_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11812289_4","volume-title":"Mathematical Knowledge Management 2006","author":"C Ballarin","year":"2006","unstructured":"Ballarin, C.: Interpretation of locales in Isabelle: theories and proof contexts. In: Borwein, J.M., Farmer, W.M. (eds.) Mathematical Knowledge Management 2006. Lecture Notes in Artificial Intelligence, pp. 31\u201343. Springer, Berlin (2006)"},{"key":"9404_CR3","unstructured":"Billingsley, P.: Probability and Measure. Wiley Series in Probability and Mathematical Statistics, A Wiley-Interscience Publication, 3rd edn. Wiley, New York (1995)"},{"key":"9404_CR4","doi-asserted-by":"crossref","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Improving real analysis in coq: a user-friendly approach to integrals and derivatives. In: Hawblitzel, C., Miller, D. (eds.) Certified Programs and Proofs\u2014-Second International Conference, CPP 2012, Kyoto, Japan, December 13\u201315, 2012. Proceedings, volume 7679 of Lecture Notes in Computer Science, pp. 289\u2013304. Springer (2012)","DOI":"10.1007\/978-3-642-35308-6_22"},{"issue":"7","key":"9404_CR5","doi-asserted-by":"publisher","first-page":"1196","DOI":"10.1017\/S0960129514000437","volume":"26","author":"S Boldo","year":"2016","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. 26(7), 1196\u20131233 (2016)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9404_CR6","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5, 56\u201368 (1940)","journal-title":"J. Symb. Logic"},{"key":"9404_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-87857-7","volume-title":"A History of the Central Limit Theorem: From Classical to Modern Probability Theory","author":"H Fischer","year":"2011","unstructured":"Fischer, H.: A History of the Central Limit Theorem: From Classical to Modern Probability Theory. Springer, New York (2011)"},{"key":"9404_CR8","doi-asserted-by":"publisher","DOI":"10.5962\/bhl.title.61710","volume-title":"Natural Inheritance","author":"F Galton","year":"1889","unstructured":"Galton, F.: Natural Inheritance. Macmillan, London (1889)"},{"key":"9404_CR9","doi-asserted-by":"crossref","unstructured":"Gottliebsen, H.: Transcendental functions and continuity checking in PVS. In: Theorem Proving in Higher-Order Logics (TPHOLs) 2000, pp. 197\u2013214. Springer, Berlin (2000)","DOI":"10.1007\/3-540-44659-1_13"},{"key":"9404_CR10","unstructured":"Hales, T., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Le Hoang, T., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the Kepler conjecture. arXiv:1501.02155"},{"key":"9404_CR11","unstructured":"Harrison, J: Formalizing basic complex analysis. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, volume 10(23) of Studies in Logic, Grammar and Rhetoric. University of Bia\u0142ystok, pp. 151\u2013165 (2007)"},{"key":"9404_CR12","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J., Heller, A.: Three chapters of measure theory in Isabelle\/HOL. In: van Eekelen, M.C.J.D., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Interactive Theorem Proving (ITP) 2011, volume 6898 of Lecture Notes in Computer Science. Springer, pp. 135\u2013151 (2011)","DOI":"10.1007\/978-3-642-22863-6_12"},{"key":"9404_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-39634-2_21","volume-title":"Interactive Theorem Proving","author":"J H\u00f6lzl","year":"2013","unstructured":"H\u00f6lzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle\/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving. Lecture Notes in Computer Science, vol. 7998, pp. 279\u2013294. Springer, Berlin (2013)"},{"key":"9404_CR14","doi-asserted-by":"crossref","unstructured":"Immler, F., Traut, C.: The flow of odes. In: Blanchette, J.C., Merz, S. (eds.) Interactive Theorem Proving\u20147th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings, volume 9807 of Lecture Notes in Computer Science. Springer, pp. 184\u2013199 (2016)","DOI":"10.1007\/978-3-319-43144-4_12"},{"issue":"1","key":"9404_CR15","first-page":"1","volume":"9","author":"R Krebbers","year":"2011","unstructured":"Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in coq. Log. Methods Comput. Sci. 9(1), 1\u201327 (2011)","journal-title":"Log. Methods Comput. Sci."},{"key":"9404_CR16","unstructured":"Mhamdi, T., Hasan, O., Tahar, S.: Formalization of entropy measures in HOL. In: van Eekelen, M.C.J.D., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Interactive Theorem Proving\u2014Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22\u201325, 2011. Proceedings, volume 6898 of Lecture Notes in Computer Science. Springer, pp. 233\u2013248 (2011)"},{"key":"9404_CR17","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL. A proof assistant for higher-order logic, volume 2283 of Lecture Notes in Computer Science. Springer, Berlin (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9404_CR18","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In: Schmidt, R.A., Schulz, S., Konev, B. (eds.) Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAAR-2010, Edinburgh, Scotland, UK, July 14, 2010, volume\u00a09 of EPiC Series. EasyChair, pp. 1\u201310 (2010)","DOI":"10.29007\/tnfd"},{"key":"9404_CR19","doi-asserted-by":"crossref","unstructured":"Qasim, M., Hasan, O., Elleuch, M., Tahar, S.: Formalization of normal random variables in HOL. In: Kohlhase, M., Johansson, M., Miller, B.R., de Moura, L., Tompa, F.W. (eds.) Intelligent Computer Mathematics\u20149th International Conference, CICM 2016, Bialystok, Poland, July 25\u201329, 2016, Proceedings, volume 9791 of Lecture Notes in Computer Science. Springer, pp. 44\u201359 (2016)","DOI":"10.1007\/978-3-319-42547-4_4"},{"key":"9404_CR20","unstructured":"Serafin, L.: A formally verified proof of the Central Limit Theorem. Master\u2019s thesis, Carnegie Mellon University (2015)"},{"key":"9404_CR21","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0028402","volume-title":"Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201997)","author":"M Wenzel","year":"1997","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E., Felty, A. (eds.) Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201997), pp. 307\u2013322. Murray Hill, New Jersey (1997)"},{"key":"9404_CR22","unstructured":"Wenzel, M.: Isabelle\/Isar\u2014a versatile environment for human-readable formal proof documents. Ph.D. thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2002)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9404-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9404-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9404-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T03:26:06Z","timestamp":1749957966000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9404-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,8]]},"references-count":22,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,12]]}},"alternative-id":["9404"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9404-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,2,8]]},"assertion":[{"value":"19 July 2016","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 January 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 February 2017","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}