Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> The Riemann integral <s> 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. <s> BIB001 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> The Riemann integral <s> 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. <s> BIB002 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> The Riemann integral <s> 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. <s> BIB003 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> The Riemann integral <s> 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. <s> BIB004 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> The Riemann integral <s> 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. <s> BIB005 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> The Riemann integral <s> 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. <s> BIB006 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> The Riemann integral <s> 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. <s> BIB007
To define the Riemann integrability in Coq,  defines the integral on step functions and then uses the traditional ε-δ definition: The value of the integral is then defined as the limit of ϕ when ε → 0. As with derivatives, the Riemann integral in Coq needs a proof that the function is integrable. PVS  ) and Mizar (Endou and Korni lowicz 1999) define integrability as the convergence of Riemann sums S(f, σ, ξ) = n i=0 (σ i+1 − σ i )f (ξ i ) where σ and ξ are finite sequences such that ∀i ∈ [[0, n]], σ i ≤ ξ i ≤ σ i+1 . Both definitions are mathematically equivalent. Coq's formula, however, cannot be used to effectively compute the value of the integral. C-CoRN defines the Riemann integral between a and b, a ≤ b, for uniformly continuous functions as the limit of the sequence of Riemann sums where σ = (a + k · b−a n+1 ) 0≤k≤n+1 and ξ = (a+k· b−a n+1 ) 0≤k≤n . As with convergence, there is a problem with naming: C-CoRN names these sums "Darboux sums" instead of "Riemann sums". The library provides no notion of integrability because C-CoRN defines the integral only for uniformly continuous functions. MathClasses defines the Riemann integral too. It even defines the Stieltjes integral (O'Connor and Spitters 2010). First, step functions and partitions are defined. Then, using several monads including the completion monad, step functions are lifted to define integrable functions. As with other constructs of MathClasses, the integral can be effectively computed.  If we restrict functions g to constant functions, this is equivalent to the Riemann integral defined as the limit of Riemann sums. 4.3.3. Measure theory and the Lebesgue integral HOL4 BIB002 , Isabelle/HOL BIB004 , Mizar, and PVS, provide a library about measure theory and use it to define integrals and probability theory. These two formalizations first define a σ-algebra A of a set X as follows: A measure µ : (X, A) → R ∪ {+∞} is defined as These definitions require the use of extended real numbers. HOL4 and Isabelle/HOL provides R = R ∪ {+∞, −∞} as an algebraic datatype. Order, addition, and multiplication, are defined on it. PVS only provides the notion of nonnegative extended reals as pairs of a Boolean and a real number, since it is sufficient for defining a measure. Moreover, addition and multiplication are easier to define for R ∪ {+∞} than for R. In these formalizations, integrals are defined for simple functions as and for nonnegative functions as f dµ = sup g dµ g is a simple function and g ≤ f except on a null set . (17) Finally, a function f is integrable if the integrals of both f + = max{f, 0} and f − = max{−f, 0} are finite. Its value is then In all these formalizations, the Lebesgue integral is defined using these integrals on the σ-algebra generated by intervals and using the Lebesgue measure generated by λ ([a; b]) = b − a. Measure theory is also used to formalized probabilities in these systems. The approach of HOL Light is slightly different. The measure of a set is defined as the Gauge integral of the constant function 1 over this set. Moreover, a function is measurable if there is a sequence of continuous functions that converges toward it except on a negligible set BIB006 . ACL2(r) provides a formalization of Lebesgue measure, but only proves that there exists some set of real numbers without Lebesgue measure BIB003 . There is no integral in this system. 4.3.4. Fundamental Theorem of Calculus All the systems that define an integral provide a proof, under various conditions, of one of these relations between derivative and integral: Formula (19) is the Fundamental Theorem of Calculus. This theorem is proved in all the surveyed formalizations for their main integral  BIB007  BIB001   BIB005 ) except Coq's standard library. Except for systems using Gauge integrals, the theorem requires that f be continuous on the interval [a; b] . In Coq's standard library, due to difficulties to work with partial functions, (20) requires that f be continuous on [a; b] with b > x, rather than just continuous at point x and integrable around it. Note that this library also provides the definition of the Newton integral (i.e. a function g is Newton integrable if there is a function f differentiable such that f = g). For this particular integral, (19) is the definition of the integral of g.