Formalization of Real Analysis: A Survey of Proof Assistants and Libraries
---
paper_title: Semi-Automated Mathematics

paper_content:

The fifth in a series of experiments in semi-automated mathematics is described. These experiments culminated in large complex computer programs which allow a mathematician to prove mathematical theorems on an man/machine basis. SAM V, the fifth program, is oriented primarily toward the development of efficient automatic techniques for handling some of the more basic processes of mathematical deduction, and toward the realization of efficient real-time interaction between man and machine through the use of cathode-ray tube displays. SAM V's most notable success is the solution of an open problem in lattice theory.
---
paper_title: Statistics on digital libraries of mathematics

paper_content:

We present statistics on the standard libraries of four major proof assistants for mathematics: HOL Light, Isabelle/HOL, Coq and Mizar. The advent of digital computers has introduced a new way of doing mathematics called 'formalized mathematics'. In this style of doing mathematics one encodes the mathematics in the computer in sufficient detail that the computer can fully check the correctness according to a small number of logical rules. This style of doing mathematics is much more precise and trustable than the traditional way of first understanding the mathematics in one's head and then just writing it on a blackboard or on paper. Also it is a very pleasurable experience to write down one's mathematics in a way that all the details are there, knowing that there is nothing left implicit. However, these positive aspects of formalized mathematics have to be paid for. Generally it takes much longer to turn mathematics into formalized form than it takes to just understand it, or even than to write it down in a traditional way. (A rough estimate might be that it takes about ten times as long to formalize something than it takes to write it down in meticulous traditional 'textbook style'.) One might wonder where this time is going, i.e., how much it is spent on the various aspects of formalization. For instance there are the aspects of formalizing the definitions, choosing good notation for the defined notions, then stating the appropriate formal statements to be proved, and finally writing the formal proofs themselves. Another question that might be posed is whether there are significant differ- ences in the time needed for these activities between the different systems for formalization of mathematics. In this paper we will study these questions. We will not do this by focusing on the activity of formalization, but rather by studying the results of this activity, the libraries of formalized mathematics that have been created by the various research communities that work on this subject. These libraries have grown into quite large human 'artifacts', which - we claim - deserve study in their own right. In this
---
paper_title: Computer-Aided Reasoning: An Approach

paper_content:

From the Publisher: ::: An Approach ::: Computer-Aided Reasoning: An Approach is a textbook introduction to computer-aided reasoning. It can be used in graduate and upper-division undergraduate courses on software engineering or formal methods. It is also suitable in conjunction with other books in courses on hardware design, discrete mathematics, or theory, especially courses stressing formalism, rigor, or mechanized support. It is also appropriate for courses on artificial intelligence or automated reasoning and as a reference for business and industry. ::: Current hardware and software systems are often very complex and the trend is towards increased complexity. Many of these systems are of critical importance; therefore making sure that they behave as expected is also of critical importance. By modeling computing systems mathematically, we obtain models that we can prove behave correctly. The complexity of computing systems makes such proofs very long, complicated, and error-prone. To further increase confidence in our reasoning, we can use a computer program to check our proofs and even to automate some of their construction. ::: In this book we present: ::: ::: A practical functional programming language closely related to Common Lisp which is used to define functions (which can model computing systems) and to make assertions about defined functions; A formal logic in which defined functions correspond to axioms; the logic is first-order, includes induction, and allows us to prove theorems about the functions; The computer-aided reasoning system ACL2, which includes the programming language, the logic, and mechanical support for the proof process. ::: ::: The ACL2 system hasbeen successfully applied to projects of commercial interest, including microprocessor, modeling, hardware verification, microcode verification, and software verification. This book gives a methodology for modeling computing systems formally and for reasoning about those models with mechanized assistance. The practicality of computer-aided reasoning is further demonstrated in the companion book, Computer-Aided Reasoning: ACL2 Case Studies. ::: Approximately 140 exercises are distributed throughout the book. Additional material is freely available from the ACL2 home page on the Web, http://www.cs.utexas.edu/users/moore/ac12, including solutions to the exercises, additional exercises, case studies from the companion book, research papers, and the ACL2 system with detailed documentation. ::: ::: ACL2 Case Studies ::: Computer-Aided Reasoning: ACL2 Case Studies illustrates how the computer-aided reasoning system ACL2 can be used in productive and innovative ways to design, build, and maintain hardware and software systems. Included here are technical papers written by twenty-one contributors that report on self-contained case studies, some of which are sanitized industrial projects. The papers deal with a wide variety of ideas, including floating-point arithmetic, microprocessor simulation, model checking, symbolic trajectory evaluation, compilation, proof checking, real analysis, and several others. ::: Computer-Aided Reasoning: ACL2 Case Studies is meant for two audiences: those looking for innovative ways to design, build, and maintain hardware and software systems faster and more reliably, and those wishing to learn how to do this. The former audience includes project managers and students in survey-oriented courses. The latter audience includes students and professionals pursuing rigorous approaches to hardware and software engineering or formal methods. Computer-Aided Reasoning: ACL2 Case Studies can be used in graduate and upper-division undergraduate courses on Software Engineering, Formal Methods, Hardware Design, Theory of Computation, Artificial Intelligence, and Automated Reasoning. ::: The book is divided into two parts. Part I begins with a discussion of the effort involved in using ACL2. It also contains a brief introduction to the ACL2 logic and its mechanization, which is intended to give the reader sufficient background to read the case studies. A more thorough, textbook introduction to ACL2 may be found in the companion book, Computer-Aided Reasoning: An Approach. ::: The heart of the book is Part II, where the case studies are presented. The case studies contain exercises whose solutions are on the Web. In addition, the complete ACL2 scripts necessary to formalize the models and prove all the properties discussed are on the Web. For example, when we say that one of the case studies formalizes a floating-point multiplier and proves it correct, we mean that not only can you read an English description of the model and how it was proved correct, but you can obtain the entire formal content of the project and replay the proofs, if you wish, with your copy of ACL2. ::: ACL2 may be obtained from its home page, http://www.cs.utexas.edu/users/moore/ac12. The results reported in each case study, as ACL2 input scripts, as well as exercise solutions for both books, are available from this page.
---
paper_title: Nonstandard Analysis in ACL2

paper_content:

ACL2 refers to a mathematical logic based on applicative Common Lisp, as well as to an automated theorem prover for this logic. The numeric system of ACL2 reflects that of Common Lisp, including the rational and complex-rational numbers and excluding the real and complex irrationals. In conjunction with the arithmetic completion axioms, this numeric type system makes it possible to prove the nonexistence of specific irrational numbers, such as √2. This paper describes ACL2(r), a version of ACL2 with support for the real and complex numbers. The modifications are based on nonstandard analysis, which interacts better with the discrete flavor of ACL2 than does traditional analysis.
---
paper_title: Subtypes for Specifications: Predicate Subtyping in PVS

paper_content:

A specification language used in the context of an effective theorem prover can provide novel features that enhance precision and expressiveness. In particular, type checking for the language can exploit the services of the theorem prover. We describe a feature called "predicate subtyping" that uses this capability and illustrate its utility as mechanized in PVS.
---
paper_title: HOL Light: An Overview

paper_content:

HOL Light is an interactive proof assistant for classical higher-order logic, intended as a clean and simplified version of Mike Gordon's original HOL system. Theorem provers in this family use a version of ML as both the implementation and interaction language; in HOL Light's case this is Objective CAML (OCaml). Thanks to its adherence to the so-called `LCF approach', the system can be extended with new inference rules without compromising soundness. While retaining this reliability and programmability from earlier HOL systems, HOL Light is distinguished by its clean and simple design and extremely small logical kernel. Despite this, it provides powerful proof tools and has been applied to some non-trivial tasks in the formalization of mathematics and industrial formal verification.
---
paper_title: Towards Self-verification of HOL Light

paper_content:

The HOL Light prover is based on a logical kernel consisting of about 400 lines of mostly functional Ocaml. whose complete formal verification seems to be quite feasible. We would like to formally verify (i) that the abstract HOL logic is indeed correct, and (ii) that the OCaml code does correctly implement this logic. We have performed a full verification of an imperfect but quite detailed model of the basic HOL Light core, without definitional mechanisms, and this verification is entirely conducted with respect to a set-theoretic semantics within HOL Light itself. We will duly explain why the obvious logical and pragmatic difficulties do not vitiate this approach, even though it looks impossible or useless at first sight. Extension to include definitional mechanisms seems straightforward enough, and the results so far allay most of our practical worries.
---
paper_title: Introduction to HOL: a theorem proving environment for higher order logic

paper_content:

Part I. Tutorial: 1. Introduction to ML 2. The HOL logic 3. Introduction to proof with HOL 4. Goal-oriented proof: tactics and tacticals 5. Example: a simple parity checker 6. How to program a proof tool 7. Example: the binomial theorem Part II. The Meta-Language ML: 8. The history of ML 9. Introduction and examples 10. Syntax of ML 11. Semantics of ML 12. ML types 13. Primitive ML identifier bindings 14. General purpose and list processing functions 15. ML system functions Part III. The Hol Logic: 16. Syntax and semantics 17. Theories Part IV. The Hol System: 18. The HOL logic in ML Part V. Theorem-Proving With HOL: 19. Derived inference rules 20. Conversions 21. Goal-directed proof: tactics and tacticals Appendices.
---
paper_title: Dense Sphere Packings: A Blueprint for Formal Proofs

paper_content:

The 400-year-old Kepler conjecture asserts that no packing of congruent balls in three dimensions can have a density exceeding the familiar pyramid-shaped cannonball arrangement. In this book, a new proof of the conjecture is presented that makes it accessible for the first time to a broad mathematical audience. The book also presents solutions to other previously unresolved conjectures in discrete geometry, including the strong dodecahedral conjecture on the smallest surface area of a Voronoi cell in a sphere packing. This book is also currently being used as a blueprint for a large-scale formal proof project, which aims to check every logical inference of the proof of the Kepler conjecture by computer. This is an indispensable resource for those who want to be brought up to date with research on the Kepler conjecture.
---
paper_title: The HOL Light Theory of Euclidean Space

paper_content:

We describe the library of theorems about N-dimensional Euclidean space that has been formalized in the HOL Light prover. This formalization was started in 2005 and has been extensively developed since then, partly in direct support of the Flyspeck project, partly out of a general desire to develop a well-rounded and comprehensive theory of basic analytical, geometrical and topological machinery. The library includes various `big name' theorems (Brouwer's fixed point theorem, the Stone-Weierstrass theorem, the Tietze extension theorem), numerous non-trivial results that are useful in applications (second mean value theorem for integrals, power series for real and complex transcendental functions) and a host of supporting definitions and lemmas. It also includes some specialized automated proof tools. The library has as planned been applied to the Flyspeck project and has become the basis of a significant development of results in complex analysis, among others.
---
paper_title: On the Mechanization of Real Analysis in Isabelle/HOL

paper_content:

Our recent, and still ongoing, development of real analysis in Isabelle/HOL is presented and compared, whenever instructive, to the one present in the theorem prover HOL. While most existing mechanizations of analysis only use the classical Ɛ and δ approach, ours uses notions from both Nonstandard Analysis and classical analysis. The overall result is an intuitive, yet rigorous, development of real analysis, and a relatively high degree of proof automation in many cases.
---
paper_title: Interactive Theorem Proving and Program Development: Coq'Art The Calculus of Inductive Constructions

paper_content:

A practical introduction to the development of proofs and certified programs using Coq. An invaluable tool for researchers, students, and engineers interested in formal methods and the development of zero-fault software.
---
paper_title: Elements of Mathematical Analysis in PVS

paper_content:

This paper presents the formalization of some elements of mathematical analysis using the PVS verification system. Our main motivation was to extend the existing PVS libraries and provide means of modelling and reasoning about hybrid systems. The paper focuses on several important aspects of PVS including recent extensions of the type system and discusses their merits and effectiveness. We conclude by a brief comparison with similar developments using other theorem provers.
---
paper_title: A Monadic, Functional Implementation of Real Numbers

paper_content:

Large scale real number computation is an essential ingredient in several modern mathematical proofs. Because such lengthy computations cannot be verified by hand, some mathematicians want to use software proof assistants to verify the correctness of these proofs. This paper develops a new implementation of the constructive real numbers and elementary functions for such proofs by using the monad properties of the completion operation on metric spaces. Bishop and Bridges's notion (Bishop and Bridges 1985) of regular sequences is generalised to what I call regular functions, which form the completion of any metric space. Using the monad operations, continuous functions on length spaces (which are a common subclass of metric spaces) are created by lifting continuous functions on the original space. A prototype Haskell implementation has been created. I believe that this approach yields a real number library that is reasonably efficient for computation, and still simple enough to verify its correctness easily.
---
paper_title: Real Number Calculations and Theorem Proving

paper_content:

When handling proofs of properties in the real world we often need to assert that one numeric quantity is greater than another. When these numeric quantities are real-valued, it is often tempting to get out the calculator to calculate the values of the expressions and then enter the results directly into the theorem prover as "facts" or axioms, since formally proving the desired properties can often be very tiresome. Obviously, such a procedure poses a few risks. ::: ::: An alternative approach, presented in this paper, is to prove the correctness of an arbitrarily accurate calculator for the reals. If this calculator is expressed in terms of the underlying integer arithmetic operations of the theorem-prover's implementation language, then there is a reasonable expectation that a practical evaluator of real-valued expressions may have been constructed. ::: ::: Obviously, there are some constraints imposed by computability theory. It is well known, for example, that it is not possible to determine the sign of a computable real in finite time. We show that for all practical purposes, we need not worry about such fussy details. After all, mathematicians have --- throughout the centuries --- been prepared to make such calculations without being overly punctilious about the computability of the operations they were performing! ::: ::: We report on the experience of validating and using a real number calculator in PVS.
---
paper_title: An Irrational Construction of R from Z

paper_content:

This paper reports on a construction of the real numbers in the ProofPower implementation of the HOL logic. Since the original construction was implemented, some major improvements to the ideas have been discovered. The improvements involve some entertaining mathematics: it turns out that the Dedekind cuts provide many routes one can travel to get from the ring of integers, Z, to the field of real numbers, R. The traditional stop-over on the way is the field of rational numbers, Q. This paper shows that going via certain rings of algebraic numbers can provide a pleasant alternative to the more well-trodden track.
---
paper_title: Constructing the real numbers in HOL

paper_content:

This paper describes a construction of the real numbers in the HOL theorem-prover by strictly definitional means using a version of Dedekind's method. It also outlines the theory of mathematical analysis that has been built on top of it and discusses current and potential applications in verification and computer algebra.
---
paper_title: Nonstandard Analysis in ACL2

paper_content:

ACL2 refers to a mathematical logic based on applicative Common Lisp, as well as to an automated theorem prover for this logic. The numeric system of ACL2 reflects that of Common Lisp, including the rational and complex-rational numbers and excluding the real and complex irrationals. In conjunction with the arithmetic completion axioms, this numeric type system makes it possible to prove the nonexistence of specific irrational numbers, such as √2. This paper describes ACL2(r), a version of ACL2 with support for the real and complex numbers. The modifications are based on nonstandard analysis, which interacts better with the discrete flavor of ACL2 than does traditional analysis.
---
paper_title: Elements of Mathematical Analysis in PVS

paper_content:

This paper presents the formalization of some elements of mathematical analysis using the PVS verification system. Our main motivation was to extend the existing PVS libraries and provide means of modelling and reasoning about hybrid systems. The paper focuses on several important aspects of PVS including recent extensions of the type system and discusses their merits and effectiveness. We conclude by a brief comparison with similar developments using other theorem provers.
---
paper_title: Real sequences and basic operations on them

paper_content:

The articles [6], [8], [1], [7], [4], [9], [2], [5], [10], and [3] provide the notation and terminology for this paper. For simplicity, we adopt the following convention: f is a function, n is a natural number, r, p are real numbers, and x is a set. A sequence of real numbers is a function from N into R. In the sequel s1, s2, s3, s4, s1, s ′ 2 denote sequences of real numbers. We now state two propositions:
---
paper_title: Functional sequence from a domain to a domain

paper_content:

Summary. Definitions of functional sequences and basic operations on functional sequences from a domain to a domain, point and uniform convergent, limit of functional sequence from a domain to the set of real numbers and facts about properties of the limit of functional sequences are proved.
---
paper_title: An Irrational Construction of R from Z

paper_content:

This paper reports on a construction of the real numbers in the ProofPower implementation of the HOL logic. Since the original construction was implemented, some major improvements to the ideas have been discovered. The improvements involve some entertaining mathematics: it turns out that the Dedekind cuts provide many routes one can travel to get from the ring of integers, Z, to the field of real numbers, R. The traditional stop-over on the way is the field of rational numbers, Q. This paper shows that going via certain rings of algebraic numbers can provide a pleasant alternative to the more well-trodden track.
---
paper_title: Convergent sequences and the limit of sequences

paper_content:

(Def. 2) There exists r such that for every y such that y ∈ dom f holds r < f (y). Let us consider s1. Let us observe that s1 is upper bounded if and only if: (Def. 3) There exists r such that for every n holds s1(n) < r. Let us observe that s1 is lower bounded if and only if: 1 The propositions (1) and (2) have been removed. 2 The proposition (5) has been removed. 3 The proposition (8) has been removed.
---
paper_title: Type Classes and Filters for Mathematical Analysis in Isabelle/HOL

paper_content:

The theory of analysis in Isabelle/HOL derives from earlier formalizations that were limited to specific concrete types: ℝ, ℂ and ℝn. Isabelle's new analysis theory unifies and generalizes these earlier efforts. The improvements are centered on two primary contributions: a generic theory of limits based on filters, and a new hierarchy of type classes that includes various topological, metric, vector, and algebraic spaces. These let us apply many results in multivariate analysis to types which are not Euclidean spaces, such as the extended real numbers, bounded continuous functions, or finite maps.
---
paper_title: Nonstandard Analysis in ACL2

paper_content:

ACL2 refers to a mathematical logic based on applicative Common Lisp, as well as to an automated theorem prover for this logic. The numeric system of ACL2 reflects that of Common Lisp, including the rational and complex-rational numbers and excluding the real and complex irrationals. In conjunction with the arithmetic completion axioms, this numeric type system makes it possible to prove the nonexistence of specific irrational numbers, such as √2. This paper describes ACL2(r), a version of ACL2 with support for the real and complex numbers. The modifications are based on nonstandard analysis, which interacts better with the discrete flavor of ACL2 than does traditional analysis.
---
paper_title: Constructing the real numbers in HOL

paper_content:

This paper describes a construction of the real numbers in the HOL theorem-prover by strictly definitional means using a version of Dedekind's method. It also outlines the theory of mathematical analysis that has been built on top of it and discusses current and potential applications in verification and computer algebra.
---
paper_title: Functions and their basic properties

paper_content:

The definitions of the mode Function and the graph of a function are introduced. The graph of a function is defined to be identical with the function. The following concepts are also defined: the domain of a function, the range of a function, the identity function, the composition of functions, the 1-1 function, the inverse function, the restriction of a function, the image and the inverse image. Certain basic facts about functions and the notions defined in the article are proved.
---
paper_title: Elements of Mathematical Analysis in PVS

paper_content:

This paper presents the formalization of some elements of mathematical analysis using the PVS verification system. Our main motivation was to extend the existing PVS libraries and provide means of modelling and reasoning about hybrid systems. The paper focuses on several important aspects of PVS including recent extensions of the type system and discusses their merits and effectiveness. We conclude by a brief comparison with similar developments using other theorem provers.
---
paper_title: Partial Functions in ACL2

paper_content:

We describe a method for introducing “partial functions” into ACL2, that is, functions not defined everywhere. The function “definitions” are actually admitted via the encapsulation principle: the new function symbol is constrained to satisfy the appropriate equation. This is permitted only when a witness function can be exhibited, establishing that the constraint is satisfiable. Of particular interest is the observation that every tail recursive definition can be witnessed in ACL2. We describe a macro that allows the convenient introduction of arbitrary tail recursive functions, and we discuss how such functions can be used to prove theorems about state machine models without reasoning about “clocks” or counting the number of steps until termination. Our macro for introducing “partial functions” also permits a variety of other recursive schemes, and we briefly illustrate some of them.
---
paper_title: The limit of a real function at a point

paper_content:

Summary. We define the proper and the improper limit of a real function at a point. The main properties of the operations on the limit of a function are proved. The connection between the one-side limits and the limit of a function at a point are exposed. Equivalent Cauchy and Heine characterizations of the limit of a real function at a point are proved.
---
paper_title: A HOL theory of Euclidean space

paper_content:

We describe a formalization of the elementary algebra, topology and analysis of finite-dimensional Euclidean space in the HOL Light theorem prover. (Euclidean space is R N with the usual notion of distance.) A notable feature is that the HOL type system is used to encode the dimension N in a simple and useful way, even though HOL does not permit dependent types. In the resulting theory the HOL type system, far from getting in the way, naturally imposes the correct dimensional constraints, e.g. checking compatibility in matrix multiplication. Among the interesting later developments of the theory are a partial decision procedure for the theory of vector spaces (based on a more general algorithm due to Solovay) and a formal proof of various classic theorems of topology and analysis for arbitrary N-dimensional Euclidean space, e.g. Brouwer's fixpoint theorem and the differentiability of inverse functions.
---
paper_title: Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives ⋆

paper_content:

Verification of numerical analysis programs requires dealing with derivatives and integrals. High confidence in this process can be achieved using a formal proof checker, such as Coq. Its standard library provides an axiomatization of real numbers and various lemmas about real analysis, which may be used for this purpose. Unfortunately, its definitions of derivative and integral are unpractical as they are partial functions that demand a proof term. This proof term makes the handling of mathematical formulas cumbersome and does not conform to traditional analysis. Other proof assistants usually do not suffer from this issue; for instance, they may rely on Hilbert's epsilon to get total operators. In this paper, we propose a way to define total operators for derivative and integral without having to extend Coq's standard axiomatization of real numbers. We proved the compatibility of our definitions with the standard library's in order to leverage existing results. We also greatly improved automation for real analysis proofs that use Coq standard definitions. We exercised our approach on lemmas involving iterated partial derivatives and differentiation under the integral sign, that were missing from the formal proof of a numerical program solving the wave equation.
---
paper_title: On the Mechanization of Real Analysis in Isabelle/HOL

paper_content:

Our recent, and still ongoing, development of real analysis in Isabelle/HOL is presented and compared, whenever instructive, to the one present in the theorem prover HOL. While most existing mechanizations of analysis only use the classical Ɛ and δ approach, ours uses notions from both Nonstandard Analysis and classical analysis. The overall result is an intuitive, yet rigorous, development of real analysis, and a relatively high degree of proof automation in many cases.
---
paper_title: Real Function Continuity

paper_content:

Summary. The continuity of real functions is discussed. There is a function defined on some domain in real numbers which is continuous in a single point and on a subset of domain of the function. Main properties of real continuous functions are proved. Among them there is the Weierstras Theorem. Algebraic features for real continuous functions are shown. Lipschitzian functions are introduced. The Lipschitz condition entails continuity.
---
paper_title: Computer-Aided Reasoning: Acl2 Case Studies

paper_content:

Preface. 1. Introduction. I: Preliminaries. 2. Overview. 3. Summaries of the Case Studies. 4. ACL2 Essentials. II: Case Studies. 5. An Exercise in Graph Theory J.S. Moore. 6. Modular Proof: The Fundamental Theorem of Calculus M. Kaufmann. 7. Mu-Calculus Model-Checking P. Manolios. 8. High-Speed, Analyzable Simulators D. Greve, et al. 9. Verification of a Simple Pipelined Machine Model J. Sawada. 10. The DE Language. 11. Using Macros to Mimic VHDL D. Borrione, et al. 12. Symbolic Trajectory Evaluation D.A. Jamsek. 13. RTL Verification: A Floating-Point Multiplier D.M. Russinoff, A. Flatau. 14. Design Verification of a Safety-Critical Embedded Verifier P. Bertoli, P. Traverso. 15. Compiler Verification Revisited W. Goerigk. 16. Ivy: A Preprocessor and Proof Checker for First-Order Logic W. McCune, O. Shumsky. 17. Knuth's Generalization of McCarthy's 91 Function J. Cowles. 18. Continuity and Differentiability R. Gamboa. Bibliography. Index.
---
paper_title: The HOL Light Theory of Euclidean Space

paper_content:

We describe the library of theorems about N-dimensional Euclidean space that has been formalized in the HOL Light prover. This formalization was started in 2005 and has been extensively developed since then, partly in direct support of the Flyspeck project, partly out of a general desire to develop a well-rounded and comprehensive theory of basic analytical, geometrical and topological machinery. The library includes various `big name' theorems (Brouwer's fixed point theorem, the Stone-Weierstrass theorem, the Tietze extension theorem), numerous non-trivial results that are useful in applications (second mean value theorem for integrals, power series for real and complex transcendental functions) and a host of supporting definitions and lemmas. It also includes some specialized automated proof tools. The library has as planned been applied to the Flyspeck project and has become the basis of a significant development of results in complex analysis, among others.
---
paper_title: Three chapters of measure theory in Isabelle/HOL

paper_content:

Currently published HOL formalizations of measure theory concentrate on the Lebesgue integral and they are restricted to realvalued measures. We lift this restriction by introducing the extended real numbers. We define the Borel s-algebra for an arbitrary type forming a topological space. Then, we introduce measure spaces with extended real numbers as measure values. After defining the Lebesgue integral and verifying its linearity and monotone convergence property, we prove the Radon-Nikodým theorem (which shows the maturity of our framework). Moreover, we formalize product measures and prove Fubini's theorem. We define the Lebesgue measure using the gauge integral available in Isabelle's multivariate analysis. Finally, we relate both integrals and equate the integral on Euclidean spaces with iterated integrals. This work covers most of the first three chapters of Bauer's measure theory textbook.
---
paper_title: Using a first order logic to verify that some set of reals has no lesbegue measure

paper_content:

This paper presents a formal proof of Vitali's theorem that not all sets of real numbers can have a Lebesgue measure, where the notion of “measure” is given very general and reasonable constraints. A careful examination of Vitali's proof identifies a set of axioms that are sufficient to prove Vitali's theorem, including a first-order theory of the reals as a complete, ordered field, “enough” sets of reals, and the axiom of choice. The main contribution of this paper is a positive demonstration that the axioms and inference rules in ACL2(r), a variant of ACL2 with support for nonstandard analysis, are sufficient to carry out this proof.
---
paper_title: A constructive formalization of the Fundamental Theorem of Calculus

paper_content:

We have finished a constructive formalization in the theorem prover Coq of the Fundamental Theorem of Calculus, which states that differentiation and integration are inverse processes. In this formalization, we have closely followed Bishop's work [4]. In this paper, we describe the formalization in some detail, focusing on how some of Bishop's original proofs had to be refined, adapted or redone from scratch.
---
paper_title: The Gauge Integral Theory in HOL4

paper_content:

The integral is one of the most important foundations for modeling dynamical systems. The gauge integral is a generalization of the Riemann integral and the Lebesgue integral and applies to a much wider class of functions. In this paper, we formalize the operational properties which contain the linearity, monotonicity, integration by parts, the Cauchy-type integrability criterion, and other important theorems of the gauge integral in higher-order logic 4 (HOL4) and then use them to verify an inverting integrator. The formalized theorem library has been accepted by the HOL4 authority and will appear in HOL4 Kananaskis-9.
---
paper_title: Computer-Aided Reasoning: An Approach

paper_content:

From the Publisher: ::: An Approach ::: Computer-Aided Reasoning: An Approach is a textbook introduction to computer-aided reasoning. It can be used in graduate and upper-division undergraduate courses on software engineering or formal methods. It is also suitable in conjunction with other books in courses on hardware design, discrete mathematics, or theory, especially courses stressing formalism, rigor, or mechanized support. It is also appropriate for courses on artificial intelligence or automated reasoning and as a reference for business and industry. ::: Current hardware and software systems are often very complex and the trend is towards increased complexity. Many of these systems are of critical importance; therefore making sure that they behave as expected is also of critical importance. By modeling computing systems mathematically, we obtain models that we can prove behave correctly. The complexity of computing systems makes such proofs very long, complicated, and error-prone. To further increase confidence in our reasoning, we can use a computer program to check our proofs and even to automate some of their construction. ::: In this book we present: ::: ::: A practical functional programming language closely related to Common Lisp which is used to define functions (which can model computing systems) and to make assertions about defined functions; A formal logic in which defined functions correspond to axioms; the logic is first-order, includes induction, and allows us to prove theorems about the functions; The computer-aided reasoning system ACL2, which includes the programming language, the logic, and mechanical support for the proof process. ::: ::: The ACL2 system hasbeen successfully applied to projects of commercial interest, including microprocessor, modeling, hardware verification, microcode verification, and software verification. This book gives a methodology for modeling computing systems formally and for reasoning about those models with mechanized assistance. The practicality of computer-aided reasoning is further demonstrated in the companion book, Computer-Aided Reasoning: ACL2 Case Studies. ::: Approximately 140 exercises are distributed throughout the book. Additional material is freely available from the ACL2 home page on the Web, http://www.cs.utexas.edu/users/moore/ac12, including solutions to the exercises, additional exercises, case studies from the companion book, research papers, and the ACL2 system with detailed documentation. ::: ::: ACL2 Case Studies ::: Computer-Aided Reasoning: ACL2 Case Studies illustrates how the computer-aided reasoning system ACL2 can be used in productive and innovative ways to design, build, and maintain hardware and software systems. Included here are technical papers written by twenty-one contributors that report on self-contained case studies, some of which are sanitized industrial projects. The papers deal with a wide variety of ideas, including floating-point arithmetic, microprocessor simulation, model checking, symbolic trajectory evaluation, compilation, proof checking, real analysis, and several others. ::: Computer-Aided Reasoning: ACL2 Case Studies is meant for two audiences: those looking for innovative ways to design, build, and maintain hardware and software systems faster and more reliably, and those wishing to learn how to do this. The former audience includes project managers and students in survey-oriented courses. The latter audience includes students and professionals pursuing rigorous approaches to hardware and software engineering or formal methods. Computer-Aided Reasoning: ACL2 Case Studies can be used in graduate and upper-division undergraduate courses on Software Engineering, Formal Methods, Hardware Design, Theory of Computation, Artificial Intelligence, and Automated Reasoning. ::: The book is divided into two parts. Part I begins with a discussion of the effort involved in using ACL2. It also contains a brief introduction to the ACL2 logic and its mechanization, which is intended to give the reader sufficient background to read the case studies. A more thorough, textbook introduction to ACL2 may be found in the companion book, Computer-Aided Reasoning: An Approach. ::: The heart of the book is Part II, where the case studies are presented. The case studies contain exercises whose solutions are on the Web. In addition, the complete ACL2 scripts necessary to formalize the models and prove all the properties discussed are on the Web. For example, when we say that one of the case studies formalizes a floating-point multiplier and proves it correct, we mean that not only can you read an English description of the model and how it was proved correct, but you can obtain the entire formal content of the project and replay the proofs, if you wish, with your copy of ACL2. ::: ACL2 may be obtained from its home page, http://www.cs.utexas.edu/users/moore/ac12. The results reported in each case study, as ACL2 input scripts, as well as exercise solutions for both books, are available from this page.
---
paper_title: On the formalization of the lebesgue integration theory in HOL

paper_content:

Lebesgue integration is a fundamental concept in many mathematical theories, such as real analysis, probability and information theory. Reported higher-order-logic formalizations of the Lebesgue integral either do not include, or have a limited support for the Borel algebra, which is the canonical sigma algebra used on any metric space over which the Lebesgue integral is defined. In this paper, we overcome this limitation by presenting a formalization of the Borel sigma algebra that can be used on any metric space, such as the complex numbers or the n-dimensional Euclidean space. Building on top of this framework, we have been able to prove some key Lebesgue integral properties, like its linearity and monotone convergence. Furthermore, we present the formalization of the “almost everywhere” relation and prove that the Lebesgue integral does not distinguish between functions which differ on a null set as well as other important results based on this concept. As applications, we present the verification of Markov and Chebyshev inequalities and the Weak Law of Large Numbers theorem.
---
paper_title: The HOL Light Theory of Euclidean Space

paper_content:

We describe the library of theorems about N-dimensional Euclidean space that has been formalized in the HOL Light prover. This formalization was started in 2005 and has been extensively developed since then, partly in direct support of the Flyspeck project, partly out of a general desire to develop a well-rounded and comprehensive theory of basic analytical, geometrical and topological machinery. The library includes various `big name' theorems (Brouwer's fixed point theorem, the Stone-Weierstrass theorem, the Tietze extension theorem), numerous non-trivial results that are useful in applications (second mean value theorem for integrals, power series for real and complex transcendental functions) and a host of supporting definitions and lemmas. It also includes some specialized automated proof tools. The library has as planned been applied to the Flyspeck project and has become the basis of a significant development of results in complex analysis, among others.
---
paper_title: Nonstandard Analysis in ACL2

paper_content:

ACL2 refers to a mathematical logic based on applicative Common Lisp, as well as to an automated theorem prover for this logic. The numeric system of ACL2 reflects that of Common Lisp, including the rational and complex-rational numbers and excluding the real and complex irrationals. In conjunction with the arithmetic completion axioms, this numeric type system makes it possible to prove the nonexistence of specific irrational numbers, such as √2. This paper describes ACL2(r), a version of ACL2 with support for the real and complex numbers. The modifications are based on nonstandard analysis, which interacts better with the discrete flavor of ACL2 than does traditional analysis.
---
paper_title: Constructing the real numbers in HOL

paper_content:

This paper describes a construction of the real numbers in the HOL theorem-prover by strictly definitional means using a version of Dedekind's method. It also outlines the theory of mathematical analysis that has been built on top of it and discusses current and potential applications in verification and computer algebra.
---
paper_title: Integer and rational exponents

paper_content:

The terminology and notation used in this paper are introduced in the following papers: [12], [15], [4], [10], [1], [2], [3], [9], [7], [8], [14], [11], [13], [6], and [5]. For simplicity we follow the rules: a, b, c will be real numbers, m, n will be natural numbers, k, l, i will be integers, p, q will be rational numbers, and s1, s2 will be sequences of real numbers. The following propositions are true: (2)2 If s1 is convergent and for every n holds s1(n) ≥ a, then lim s1 ≥ a. (3) If s1 is convergent and for every n holds s1(n) ≤ a, then lim s1 ≤ a. Let us consider a. The functor (a)κ∈ yielding a sequence of real numbers is defined as follows: (Def.1) ((a)κ∈ )(0) = 1 and for every m holds ((a)κ∈ )(m+1) = ((a)κ∈ )(m)· a.
---
paper_title: Real automation in the field

paper_content:

Abstract. We provide a package of strategies for automation of non-linear arithmetic in PVS. Inparticular, we describe a simplification procedure for the field of real numbers and a strategy for cancellationof common terms.Key words, non-linear arithmetic, PVS strategies, real number automationSubject classification. Computer Science1. Introduction. While conducting research on the formal safety analysis of Air Traffic Management(ATM) systems at the NASA Langley Research Center [2, 3, 6], we have found the verification system PVS[7] very well suited for specifying avionics systems. Avionics systems are hybrid systems, that is, they aredigital systems that interact with the continuous physical environment where they are deployed. These twolevels of dynamics, discrete and continuous, can be easily modeled using PVS higher-order logic. Despitethat, deductive methods, such as theorem proving, are not usually the first approach for modeling andverification of hybrid systems. Most of the literature on verification of hybrid systems concerns variationsof algorithmic methods, such as model checking, on restricted sub-classes of the general problem. This canbe explained by the fact that although theorem provers based on higher-order logic, e.g., PVS [7], Coq [1],Isabelle-HOL [8], integrate expressive specification languages with powerful theorem provers, they lack ofadequate support for continuous mathematics.The PVS system, for instance, incorporates a rich type system supporting predicate sub-typing anddependent types. It also comes with a set of decision procedures that solve problems in a broad range ofdecidable fields. Moreover, it includes in the prelude library a large collection of properties for real numbers(for example, real_props and real_axioms) that are applied automatically by the decision procedures.This is true except for non-linear ones, i.e., those involving multiplication or division of non-numeric terms.Indeed, the PVS command (GRIND :theories "real_props"), although useful in several cases, fails todischarge a simple non-linear formula such as(1.1) aa+_+ 1 - b -- 1
---
paper_title: Proving Equalities in a Commutative Ring Done Right in Coq

paper_content:

We present a new implementation of a reflexive tactic which solves equalities in a ring structure inside the Coq system. The efficiency is improved to a point that we can now prove equalities that were previously beyond reach. A special care has been taken to implement efficient algorithms while keeping the complexity of the correctness proofs low. This leads to a single tool, with a single implementation, which can be addressed for a ring or for a semi-ring, abstract or not, using the Leibniz equality or a setoid equality. This example shows that such reflective methods can be effectively used in symbolic computation.
---
paper_title: Verifying nonlinear real formulas via sums of squares

paper_content:

Techniques based on sums of squares appear promising as a general approach to the universal theory of reals with addition and multiplication, i.e. verifying Boolean combinations of equations and inequalities. A particularly attractive feature is that suitable 'sum of squares' certificates can be found by sophisticated numerical methods such as semidefinite programming, yet the actual verification of the resulting proof is straightforward even in a highly foundational theorem prover. We will describe our experience with an implementation in HOL Light, noting some successes as well as difficulties. We also describe a new approach to the univariate case that can handle some otherwise difficult examples.
---
paper_title: Formalization of Bernstein Polynomials and Applications to Global Optimization

paper_content:

This paper presents a formalization in higher-order logic of a practical representation of multivariate Bernstein polynomials. Using this representation, an algorithm for finding lower and upper bounds of the minimum and maximum values of a polynomial has been formalized and verified correct in the Prototype Verification System (PVS). The algorithm is used in the definition of proof strategies for formally and automatically solving polynomial global optimization problems.
---
paper_title: Fast Reflexive Arithmetic Tactics the linear case and beyond

paper_content:

When goals fall in decidable logic fragments, users of proof-assistants expect automation. However, despite the availability of decision procedures, automation does not come for free. The reason is that decision procedures do not generate proof terms. In this paper, we show how to design efficient and lightweight reflexive tactics for a hierarchy of quantifier-free fragments of integer arithmetics. The tactics can cope with a wide class of linear and non-linear goals. For each logic fragment, off-the-shelf algorithms generate certificates of infeasibility that are then validated by straightforward reflexive checkers proved correct inside the proof-assistant. This approach has been prototyped using the Coq proofassistant. Preliminary experiments are promising as the tactics run fast and produce small proof terms.
---
paper_title: A proof-producing decision procedure for real arithmetic

paper_content:

We present a fully proof-producing implementation of a quantifier elimination procedure for real closed fields. To our knowledge, this is the first generally useful proof-producing implementation of such an algorithm. While many problems within the domain are intractable, we demonstrate convincing examples of its value in interactive theorem proving.
---
paper_title: Verifying mixed real-integer quantifier elimination

paper_content:

We present a formally verified quantifier elimination procedure for the first order theory over linear mixed real-integer arithmetics in higher-order logic based on a work by Weispfenning. To this end we provide two verified quantifier elimination procedures: for Presburger arithmitics and for linear real arithmetics.
---
paper_title: Verified Real Number Calculations: A Library for Interval Arithmetic

paper_content:

Real number calculations on elementary functions are remarkably difficult to handle in mechanical proofs. In this paper, we show how these calculations can be performed within a theorem prover or proof assistant in a convenient and highly automated as well as interactive way. First, we formally establish upper and lower bounds for elementary functions. Then, based on these bounds, we develop a rational interval arithmetic where real number calculations take place in an algebraic setting. In order to reduce the dependency effect of interval arithmetic, we integrate two techniques: interval splitting and Taylor series expansions. This pragmatic approach has been developed, and formally verified, in a theorem prover. The formal development also includes a set of customizable strategies to automate proofs involving explicit calculations over real numbers. Our ultimate goal is to provide guaranteed proofs of numerical properties with minimal human theorem-prover interaction.
---
paper_title: On the Generation of Positivstellensatz Witnesses in Degenerate Cases

paper_content:

One can reduce the problem of proving that a polynomial is nonnegative, or more generally of proving that a system of polynomial inequalities has no solutions, to finding polynomials that are sums of squares of polynomials and satisfy some linear equality (Positivstellensatz). This produces a witness for the desired property, from which it is reasonably easy to obtain a formal proof of the property suitable for a proof assistant such as Coq. The problem of finding a witness reduces to a feasibility problem in semidefinite programming, for which there exist numerical solvers. Unfortunately, this problem is in general not strictly feasible, meaning the solution can be a convex set with empty interior, in which case the numerical optimization method fails. Previously published methods thus assumed strict feasibility; we propose a workaround for this difficulty. We implemented our method and illustrate its use with examples, including extractions of proofs to Coq.
---
paper_title: Linear and Nonlinear Arithmetic in ACL2

paper_content:

sec:abstractAs of version 2.7, the ACL2 theorem prover has been extended to automatically verify sets of polynomial inequalities that include nonlinear relationships. In this paper we describe our mechanization of linear and nonlinear arithmetic in ACL2. The nonlinear arithmetic procedure operates in cooperation with the pre-existing ACL2 linear arithmetic decision procedure. It extends what can be automatically verified with ACL2, thereby eliminating the need for certain types of rules in ACL2’s database while simultaneously increasing the performance of the ACL2 system when verifying arithmetic conjectures. The resulting system lessens the human effort required to construct a large arithmetic proof by reducing the number of intermediate lemmas that must be proven to verify a desired theorem.
---
paper_title: Automatic differentiation in ACL2

paper_content:

In this paper, we describe recent improvements to the theory of differentiation that is formalized in ACL2(r). First, we show how the normal rules for the differentiation of composite functions can be introduced in ACL2(r). More important, we show how the application of these rules can be largely automated, so that ACL2(r) can automatically define the derivative of a function that is built from functions whose derivatives are already known. Second, we show a formalization in ACL2(r) of the derivatives of familiar functions from calculus, such as the exponential, logarithmic, power, and trigonometric functions. These results serve as the starting point for the automatic differentiation tool described above. Third, we describe how users can add new functions and their derivatives, to improve the capabilities of the automatic differentiator. In particular, we show how to introduce the derivative of the hyperbolic trigonometric functions. Finally, we give some brief highlights concerning the implementation details of the automatic differentiator.
---
paper_title: Formalizing Integration Theory with an Application to Probabilistic Algorithms

paper_content:

Inter alia, Lebesgue-style integration plays a major role in advanced probability. We formalize a significant part of its theory in Higher Order Logic using Isabelle/Isar. This involves concepts of elementary measure theory, real-valued random variables as Borel-measurable functions, and a stepwise inductive definition of the integral itself. Building on previous work about formal verification of probabilistic algorithms, we exhibit an example application in this domain; another primitive for randomized functional programming is developed to this end.
---
paper_title: Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq

paper_content:

Several formalizations of floating-point arithmetic have been designed for the Coq system, a generic proof assistant. Their different purposes have favored some specific applications: program verification, high-level properties, automation. Based on our experience using and/or developing these libraries, we have built a new system that is meant to encompass the other ones in a unified framework. It offers a multi-radix and multi-precision formalization for various floating- and fixed-point formats. This fresh setting has been the occasion for reevaluating known properties and generalizing them. This paper presents design decisions and examples of theorems from the Flocq system: a library easy to use, suitable for automation yet high-level and generic.
---
paper_title: Formalizing O Notation in Isabelle/HOL

paper_content:

We describe a formalization of asymptotic O notation using the Isabelle/HOL proof assistant.
---
paper_title: Formal Verification of Exact Computations Using Newton's Method

paper_content:

We are interested in the verification of Newton's method. We use a formalization of the convergence and stability of the method done with the axiomatic real numbers of Coq's Standard Library in order to validate the computation with Newton's method done with a library of exact real arithmetic based on co-inductive streams. The contribution of this work is twofold. Firstly, based on Newton's method, we design and prove correct an algorithm on streams for computing the root of a real function in a lazy manner. Secondly, we prove that rounding at each step in Newton's method still yields a convergent process with an accurate correlation between the precision of the input and that of the result. An algorithm including rounding turns out to be much more efficient.
---
paper_title: Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL

paper_content:

Many ordinary differential equations (ODEs) do not have a closed solution, therefore approximating them is an important problem in numerical analysis. This work formalizes a method to approximate solutions of ODEs in Isabelle/HOL.
---
paper_title: Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations

paper_content:

We present a formal tool for verification of multivariate nonlinear inequalities. Our verification method is based on interval arithmetic with Taylor approximations. Our tool is implemented in the HOL Light proof assistant and it is capable to verify multivariate nonlinear polynomial and non-polynomial inequalities on rectangular domains. One of the main features of our work is an efficient implementation of the verification procedure which can prove non-trivial high-dimensional inequalities in several seconds. We developed the verification tool as a part of the Flyspeck project (a formal proof of the Kepler conjecture). The Flyspeck project includes about 1000 nonlinear inequalities. We successfully tested our method on more than 100 Flyspeck inequalities and estimated that the formal verification procedure is about 3000 times slower than an informal verification method implemented in C++. We also describe future work and prospective optimizations for our method.
---
paper_title: A certified, corecursive implementation of exact real numbers

paper_content:

We implement exact real numbers in the logical framework Coq using streams, i.e., infinite sequences, of digits, and characterize constructive real numbers through a minimal axiomatization. We prove that our construction inhabits the axiomatization, working formally with coinductive types and corecursive proofs. Thus we obtain reliable, corecursive algorithms for computing on real numbers.
---
paper_title: Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives ⋆

paper_content:

Verification of numerical analysis programs requires dealing with derivatives and integrals. High confidence in this process can be achieved using a formal proof checker, such as Coq. Its standard library provides an axiomatization of real numbers and various lemmas about real analysis, which may be used for this purpose. Unfortunately, its definitions of derivative and integral are unpractical as they are partial functions that demand a proof term. This proof term makes the handling of mathematical formulas cumbersome and does not conform to traditional analysis. Other proof assistants usually do not suffer from this issue; for instance, they may rely on Hilbert's epsilon to get total operators. In this paper, we propose a way to define total operators for derivative and integral without having to extend Coq's standard axiomatization of real numbers. We proved the compatibility of our definitions with the standard library's in order to leverage existing results. We also greatly improved automation for real analysis proofs that use Coq standard definitions. We exercised our approach on lemmas involving iterated partial derivatives and differentiation under the integral sign, that were missing from the formal proof of a numerical program solving the wave equation.
---
paper_title: Floating Point Verification in HOL Light: The Exponential Function

paper_content:

Since they often embody compact but mathematically sophisticated algorithms, operations for computing the common transcendental functions in floating point arithmetic seem good targets for formal verification using a mechanical theorem prover. We discuss some of the general issues that arise in verifications of this class, and then present a machine-checked verification of an algorithm for computing the exponential function in IEEE-754 standard binary floating point arithmetic. We confirm (indeed strengthen) the main result of a previously published error analysis, though we uncover a minor error in the hand proof and are forced to confront several subtle issues that might easily be overlooked informally.
---
paper_title: Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program

paper_content:

We formally prove correct a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors at several levels: the numerical scheme introduces method errors, and floating-point computations lead to round-off errors. We annotate this C program to specify both method error and round-off error. We use Frama-C to generate theorems that guarantee the soundness of the code. We discharge these theorems using SMT solvers, Gappa, and Coq. This involves a large Coq development to prove the adequacy of the C program to the numerical scheme and to bound errors. To our knowledge, this is the first time such a numerical analysis program is fully machine-checked.
---
paper_title: Provably Correct Conflict Prevention Bands Algorithms

paper_content:

In air traffic management, a pairwise conflict is a predicted loss of separation between two aircraft, referred to as the ownship and the intruder. A conflict prevention bands system displays ranges of maneuvers for the ownship that characterize regions in the airspace that are either conflict-free or ''don't go'' zones that the ownship has to avoid. Errors in the calculation of prevention bands may result in incorrect separation assurance information being displayed to pilots or air traffic controllers. Algorithms that compute conflict prevention bands are surprisingly difficult to formalize and verify. This paper presents a method for the analysis and verification of prevention bands algorithms. The method, which has been implemented in the Prototype Verification System (PVS), is illustrated with a provably correct 3-dimensional (3D) prevention bands algorithm for track angle maneuvers.
---

Title: Formalization of Real Analysis: A Survey of Proof Assistants and Libraries

Section 1: Introduction
Description 1: Write an introduction to the topic, explaining the relevance and purpose of the survey, and providing some historical context. Mention the proof assistants and libraries that will be the focus.

Section 2: Proof Assistants and Libraries
Description 2: Discuss the proof assistants and libraries used in the survey, highlighting their characteristics and methodologies.

Section 3: Formalizations of Real Numbers
Description 3: Present the different formalizations of real numbers adopted by the various systems and classify them into axiomatized, constructed, and non-standard analysis.

Section 4: Formalizations of Real Analysis
Description 4: Examine how each system defines and proves common concepts of real analysis, such as sequences, series, continuity, differentiability, and integrals.

Section 5: Sequences and Series
Description 5: Explain the definitions and theorems related to sequences and series in the various formal systems, including their convergence criteria and properties.

Section 6: Functions over Real Numbers
Description 6: Describe the formalization of functions of real numbers, focusing on partial functions, limits, continuity, and differentiability.

Section 7: Integrals
Description 7: Detail the formalization of integrals, including the Riemann and Lebesgue integrals, and the Fundamental Theorem of Calculus.

Section 8: Elementary Functions
Description 8: Discuss the formalization of elementary functions like exponential, logarithm, and trigonometric functions using various methodologies.

Section 9: Methods of Automation
Description 9: Provide an overview of the automatic methods available in the proof assistants for solving real arithmetic and analysis problems.

Section 10: Conclusion
Description 10: Summarize the findings and insights from the survey, noting the strengths and limitations of each system, and the implications for users and developers.