{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,20]],"date-time":"2026-10-20T01:53:38Z","timestamp":1792461218042,"version":"4.5.0"},"reference-count":107,"publisher":"Cambridge University Press (CUP)","issue":"7","license":[{"start":{"date-parts":[[2015,1,2]],"date-time":"2015-01-02T00:00:00Z","timestamp":1420156800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2016,10]]},"abstract":"<jats:p>In the recent years, numerous proof systems have improved enough to be used for formally verifying non-trivial mathematical results. They, however, have different purposes and it is not always easy to choose which one is adapted to undertake a formalization effort. In this survey, we focus on properties related to real analysis: real numbers, arithmetic operators, limits, differentiability, integrability and so on. We have chosen to look into the formalizations provided in standard by the following systems: Coq, HOL4, HOL Light, Isabelle\/HOL, Mizar, ProofPower-HOL, and PVS. We have also accounted for large developments that play a similar role or extend standard libraries: ACL2(r) for ACL2, C-CoRN\/MathClasses for Coq, and the NASA PVS library. This survey presents how real numbers have been defined in these various provers and how the notions of real analysis described above have been formalized. We also look at the methods of automation these systems provide for real analysis.<\/jats:p>","DOI":"10.1017\/s0960129514000437","type":"journal-article","created":{"date-parts":[[2015,1,2]],"date-time":"2015-01-02T10:26:08Z","timestamp":1420194368000},"page":"1196-1233","source":"Crossref","is-referenced-by-count":38,"title":["Formalization of real analysis: a survey of proof assistants and libraries"],"prefix":"10.1017","volume":"26","author":[{"given":"SYLVIE","family":"BOLDO","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"CATHERINE","family":"LELAY","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"GUILLAUME","family":"MELQUIOND","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2015,1,2]]},"reference":[{"key":"S0960129514000437_ref17","unstructured":"Cohen C. (2012) Formalized Algebraic Numbers: Construction and First Order Theory, Ph.D. thesis, \u00c9cole Polytechnique."},{"key":"S0960129514000437_ref12","first-page":"55","article-title":"Functions and their basic properties","volume":"1","author":"Byli\u0144ski","year":"1990","journal-title":"Journal of Formalized Mathematics"},{"key":"S0960129514000437_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_43"},{"key":"S0960129514000437_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44755-5_5"},{"key":"S0960129514000437_ref61","first-page":"273","article-title":"Convergent sequences and the limit of sequences","volume":"1","author":"Kotowicz","year":"1990","journal-title":"Journal of Formalized Mathematics"},{"key":"S0960129514000437_ref21","unstructured":"Cruz-Filipe L. (2004) Constructive Real Analysis: A Type-Theoretical Formalization and Applications, Ph.D. thesis, University of Nijmegen."},{"key":"S0960129514000437_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0105402"},{"key":"S0960129514000437_ref63","first-page":"71","article-title":"The limit of a real function at a point","volume":"2","author":"Kotowicz","year":"1991","journal-title":"Journal of Formalized Mathematics"},{"key":"S0960129514000437_ref28","first-page":"281","article-title":"Definition of integrability for partial functions from \u211d to \u211d and integrability for continuous functions","volume":"9","author":"Endou","year":"2001","journal-title":"Formalized Mathematics"},{"key":"S0960129514000437_ref36","volume-title":"Introduction to HOL","author":"Gordon","year":"1993"},{"key":"S0960129514000437_ref78","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9256-3"},{"key":"S0960129514000437_ref82","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005871"},{"key":"S0960129514000437_ref101","unstructured":"Trybulec A. (1993) Some features of the Mizar language. In: Proceedings of the ESPRIT Workshop, Torino, Italy 1\u201317."},{"key":"S0960129514000437_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3188-0_18"},{"key":"S0960129514000437_ref87","first-page":"17","article-title":"Functional sequence from a domain to a domain","volume":"3","author":"Perkowska","year":"1992","journal-title":"Journal of Formalized Mathematics"},{"key":"S0960129514000437_ref100","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000119"},{"key":"S0960129514000437_ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_9"},{"key":"S0960129514000437_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.09.061"},{"key":"S0960129514000437_ref62","first-page":"269","article-title":"Real sequences and basic operations on them","volume":"1","author":"Kotowicz","year":"1990","journal-title":"Journal of Formalized Mathematics"},{"key":"S0960129514000437_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44659-1_13"},{"key":"S0960129514000437_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_22"},{"key":"S0960129514000437_ref85","first-page":"748","article-title":"PVS: A prototype verification system","volume":"607","author":"Owre","year":"1992","journal-title":"Lecture Notes in Artificial Intelligence"},{"key":"S0960129514000437_ref90","first-page":"125","article-title":"Integer and rational exponents","volume":"2","author":"Raczkowski","year":"1991","journal-title":"Journal of Formalized Mathematics"},{"key":"S0960129514000437_ref59","first-page":"27","article-title":"Computing with classical real numbers","volume":"2","author":"Kaliszyk","year":"2009","journal-title":"Journal of Automated Reasoning"},{"key":"S0960129514000437_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_7"},{"key":"S0960129514000437_ref107","first-page":"137","article-title":"Statistics on digital libraries of mathematics","volume":"18","author":"Wiedijk","year":"2009","journal-title":"Studies in Logic, Grammar and Rhetoric"},{"key":"S0960129514000437_ref49","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9250-9"},{"key":"S0960129514000437_ref53","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_14"},{"key":"S0960129514000437_ref95","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22863-6_23"},{"key":"S0960129514000437_ref7","unstructured":"Bickford M. (2008) Formalizing Constructive Analysis in Nuprl, Computing Science Department, Cornell University. Available at: http:\/\/www.nuprl.org\/MathLibrary\/ConstructiveAnalysis\/"},{"key":"S0960129514000437_ref80","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_5"},{"key":"S0960129514000437_ref103","unstructured":"Vito B. L. D. (2003) Strategy-enhanced interactive proving and arithmetic simplification for PVS. In: Proceedings of STRATA 2003, 1st International Workshop on Design and Application of Strategies\/Tactics in Higher Order Logics, number CP-2003-212448, NASA, Rome, Italy."},{"key":"S0960129514000437_ref56","first-page":"297","volume-title":"Papers Presented at the 2nd Annual Workshop on Logical Environments","author":"Jones","year":"1993"},{"key":"S0960129514000437_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_4"},{"key":"S0960129514000437_ref25","unstructured":"Desmettre O. (2002) Coq standard library \u2013 RiemannInt."},{"key":"S0960129514000437_ref11","first-page":"1","article-title":"Formalization of the integral calculus in the PVS theorem prover","volume":"2","author":"Butler","year":"2009","journal-title":"Journal of Formalized Reasoning"},{"key":"S0960129514000437_ref91","first-page":"213","article-title":"Real exponents and logarithms","volume":"2","author":"Raczkowski","year":"1991","journal-title":"Journal of Formalized Mathematics"},{"key":"S0960129514000437_ref92","first-page":"449","article-title":"Series","volume":"2","author":"Raczkowski","year":"1991","journal-title":"Journal of Formalized Mathematics"},{"key":"S0960129514000437_ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_26"},{"key":"S0960129514000437_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_7"},{"key":"S0960129514000437_ref3","first-page":"106","article-title":"Development of practical verification tools","volume":"11","author":"Arthan","year":"1996","journal-title":"ICL Systems Journal"},{"key":"S0960129514000437_ref51","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_21"},{"key":"S0960129514000437_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_23"},{"key":"S0960129514000437_ref33","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011908113514"},{"key":"S0960129514000437_ref99","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38088-4_26"},{"key":"S0960129514000437_ref57","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_28"},{"key":"S0960129514000437_ref94","first-page":"797","article-title":"Real function differentiability","volume":"1","author":"Raczkowski","year":"1990","journal-title":"Journal of Formalized Mathematics"},{"key":"S0960129514000437_ref54","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22863-6_12"},{"key":"S0960129514000437_ref52","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39724-3_29"},{"key":"S0960129514000437_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0097791"},{"key":"S0960129514000437_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45842-5_6"},{"key":"S0960129514000437_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_4"},{"key":"S0960129514000437_ref32","unstructured":"Gamboa R. , Cowles J. R. and Kuzmina N. (2004) Axiomatic events in ACL2(r): A story of defun, defun-std, and encapsulate. In: Proceedings of the 5th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, TX, USA 1\u201318."},{"key":"S0960129514000437_ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"S0960129514000437_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25984-8_27"},{"key":"S0960129514000437_ref58","unstructured":"Jutting L. S. v. B. (1977) Checking Landau's \u2018Grundlagen\u2019 in the AUTOMATH System, Ph.D. thesis, Eindhoven University of Technology."},{"key":"S0960129514000437_ref39","doi-asserted-by":"publisher","DOI":"10.1145\/321495.321500"},{"key":"S0960129514000437_ref64","first-page":"17","article-title":"The limit of a real function at infinity","volume":"2","author":"Kotowicz","year":"1991","journal-title":"Journal of Formalized Mathematics"},{"key":"S0960129514000437_ref50","unstructured":"HOL4 development team (2012) The HOL system LOGIC, Technical Report, University of Cambridge, NICTA and University of Utah."},{"key":"S0960129514000437_ref102","unstructured":"Trybulec A. (1998) Non negative real numbers. Part I. Journal of Formalized Mathematics Addenda."},{"key":"S0960129514000437_ref2","unstructured":"Arthan R. D. (2012) Mathematical Case Studies: Basic Analysis, Lemma 1 Ltd."},{"key":"S0960129514000437_ref88","unstructured":"Pottier L. (2008) Connecting Gr\u00f6bner bases programs with Coq to do proofs in algebra, geometry and arithmetics. In: Sutcliffe G. , Rudnicki P. , Schmidt R. , Konev B. and Schulz S. (eds.) Knowledge Exchange: Automated Provers and Proof Assistants, CEUR Workshop Proceedings, Doha, Qatar 67\u201376."},{"key":"S0960129514000437_ref15","first-page":"27","article-title":"Context aware calculation and deduction \u2013 ring equalities via Gr\u00f6bner bases in Isabelle","volume":"4573","author":"Chaieb","year":"2007","journal-title":"Lecture Notes in Artificial Intelligence"},{"key":"S0960129514000437_ref43","doi-asserted-by":"crossref","unstructured":"Harrison J. (1997) Floating point verification in HOL Light: The exponential function, Technical Report 428, University of Cambridge Computer Laboratory.","DOI":"10.1007\/BFb0000475"},{"key":"S0960129514000437_ref31","doi-asserted-by":"crossref","unstructured":"Gamboa R. and Cowles J. R. (2009) Inverse functions in ACL2(r) In: Proceedings of the 8th International Workshop on the ACL2 Theorem Prover and its Applications 57\u201361.","DOI":"10.1145\/1637837.1637846"},{"key":"S0960129514000437_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27818-4_7"},{"key":"S0960129514000437_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74464-1_4"},{"key":"S0960129514000437_ref98","doi-asserted-by":"publisher","DOI":"10.1155\/2013\/160875"},{"key":"S0960129514000437_ref23","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2008.213"},{"key":"S0960129514000437_ref60","volume-title":"Computer-Aided Reasoning: An Approach","author":"Kaufmann","year":"2000"},{"key":"S0960129514000437_ref41","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384233"},{"key":"S0960129514000437_ref24","unstructured":"Delahaye D. and Mayero M. (2001) Field, une proc\u00e9dure de d\u00e9cision pour les nombres r\u00e9els en Coq. In: Cast\u00e9ran P. (ed.) Journ\u00e9es Francophones des Langages Applicatifs (JFLA'01) 33\u201348."},{"key":"S0960129514000437_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44659-1_10"},{"key":"S0960129514000437_ref71","unstructured":"Mayero M. (2001) Formalisation et automatisation de preuves en analyses r\u00e9elle et num\u00e9rique, Ph.D. thesis, Universit\u00e9 Paris VI."},{"key":"S0960129514000437_ref14","first-page":"246","article-title":"Parametric linear arithmetic over ordered fields in Isabelle\/HOL","volume":"5144","author":"Chaieb","year":"2008","journal-title":"Lecture Notes in Artificial Intelligence"},{"key":"S0960129514000437_ref8","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9255-4"},{"key":"S0960129514000437_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"S0960129514000437_ref18","unstructured":"Constable R. L. , Allen S. F. , Allen S. F. , Bromley H. M. , Cleaveland W. R. , Cremer J. F. , Harper R. W. , Howe D. J. , Knoblock T. B. , Mendler N. P. , Panangaden P. , Smith S. F. , Sasaki J. T. and Smith S. F. (1986) Implementing Mathematics with the Nuprl Proof Development System, Computing Science Department, Cornell University, Ithaca, NY."},{"key":"S0960129514000437_ref45","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_8"},{"key":"S0960129514000437_ref75","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22863-6_19"},{"key":"S0960129514000437_ref65","first-page":"29","article-title":"One-side limits of a real function at a point","volume":"2","author":"Kotowicz","year":"1991","journal-title":"Journal of Formalized Mathematics"},{"key":"S0960129514000437_ref67","doi-asserted-by":"publisher","DOI":"10.1145\/1345169.1345171"},{"key":"S0960129514000437_ref86","unstructured":"Owre S. and Shankar N. (2003) The PVS Prelude Library. Technical Report, CSL Technical Report SRI-CSL-03-01."},{"key":"S0960129514000437_ref105","doi-asserted-by":"publisher","DOI":"10.1023\/A:1021935419355"},{"key":"S0960129514000437_ref40","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139193894"},{"key":"S0960129514000437_ref66","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(1:1)2013"},{"key":"S0960129514000437_ref77","unstructured":"Mu\u00f1oz C. and Mayero M. (2001) Real automation in the field. Technical Report NASA\/CR-2001-211271, ICASE."},{"key":"S0960129514000437_ref74","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_27"},{"key":"S0960129514000437_ref46","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_17"},{"key":"S0960129514000437_ref96","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30142-4_20"},{"key":"S0960129514000437_ref70","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000009505.07087.34"},{"key":"S0960129514000437_ref76","doi-asserted-by":"publisher","DOI":"10.1109\/12.713311"},{"key":"S0960129514000437_ref79","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.07.002"},{"key":"S0960129514000437_ref27","first-page":"93","article-title":"The definition of the Riemann definite integral and some related lemmas","volume":"8","author":"Endou","year":"1999","journal-title":"Journal of Formalized Mathematics"},{"key":"S0960129514000437_ref73","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_22"},{"key":"S0960129514000437_ref68","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_19"},{"key":"S0960129514000437_ref84","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.05.031"},{"key":"S0960129514000437_ref106","doi-asserted-by":"publisher","DOI":"10.1007\/11542384"},{"key":"S0960129514000437_ref72","unstructured":"Mayero M. (2012) Probl\u00e8mes critiques et preuves formelles, Habilitation \u00e0 diriger des recherches, Universit\u00e9 Paris 13."},{"key":"S0960129514000437_ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ARITH.2011.40"},{"key":"S0960129514000437_ref83","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_21"},{"key":"S0960129514000437_ref89","unstructured":"ProofPower development team (2006) Proofpower - HOL reference manual, Technical Report, Lemma 1 Ltd."},{"key":"S0960129514000437_ref104","unstructured":"Wenzel M. (2002) Isabelle\/Isar \u2013 A Versatile Environment for Human-Readable Formal Proof Documents, Ph.D. thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen."},{"key":"S0960129514000437_ref97","doi-asserted-by":"publisher","DOI":"10.1109\/32.713327"},{"key":"S0960129514000437_ref81","volume-title":"Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic","author":"Nipkow","year":"2002"},{"key":"S0960129514000437_ref93","first-page":"787","article-title":"Real function continuity","volume":"1","author":"Raczkowski","year":"1990","journal-title":"Journal of Formalized Mathematics"},{"key":"S0960129514000437_ref69","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_34"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129514000437","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,19]],"date-time":"2019-08-19T04:40:18Z","timestamp":1566189618000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129514000437\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,1,2]]},"references-count":107,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2016,10]]}},"alternative-id":["S0960129514000437"],"URL":"https:\/\/doi.org\/10.1017\/s0960129514000437","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,1,2]]}}}