Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Conclusion <s> 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. <s> BIB001 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Conclusion <s> We describe a formalization of asymptotic O notation using the Isabelle/HOL proof assistant. <s> BIB002 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Conclusion <s> 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. <s> BIB003 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Conclusion <s> 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. <s> BIB004 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Conclusion <s> 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. <s> BIB005 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Conclusion <s> 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. <s> BIB006 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Conclusion <s> 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. <s> BIB007 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Conclusion <s> 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. <s> BIB008 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Conclusion <s> 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. <s> BIB009 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Conclusion <s> 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. <s> BIB010 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Conclusion <s> 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. <s> BIB011
This variety of formalizations might cause issues for the users as some approaches are better suited for some properties and no system provides all of them. This will also be a source of concern for people interested in exchanging theorems and proofs between various formal systems, such as  for the HOL family of theorem provers. Hopefully, this survey provides enough details to help in choosing a system good enough for proving properties related to real analysis. More details on some historical and logical aspects of formalizing real numbers are detailed by  . To see how various provers deal with real analysis, one can also take a look at Wiedijk's webpage § § ; he presents 100 famous theorems (some of them from real analysis) and their formal proofs using several systems. Table 1 . Formalizations of real analysis at a glance. The "logic" row gives a simplified vision of the logical framework: "deptypes" stands for dependent types, "constr" for constructive, and "ZF" for the Zermelo-Fraenkel set theory. The "partial functions" row is closely related, as it explains how partial functions are handled, e.g. division or derivative. The "definition of reals" row summarizes how real numbers are defined: "Cauchy sequences" and "Dedekind cuts" mean that they are built accordingly; "axiomatic" means that they are given by axioms; "non-std analysis" means that the real numbers are built given axiomatized non-standard predicates; "UF" means that there are non-standard reals built using the ultrafilter construction. The "integrals" row tells which definitions of integral are available. The "multivariate analysis" row describes its availability: "1D" means one-dimension only; "2D" means some results have been extended to R 2 ; "nD" means a proper multivariate analysis; "nD+" means that some results are available for topological spaces other than R n . The "dedicated automation" row tries to evaluate the number, power, and breadth of automatic methods for real numbers and real analysis: the more "+" the better. One of the lessons learned is that real analysis in ACL2(r) is not as developed as in other systems. Moreover, the absence of higher-order logic makes it difficult to manipulate functions. As such, this system should be reserved to users who have to interface with other ACL2 developments. Let us now examine the other systems. If one is not interested in topology and metric spaces, the extent of the provided libraries is mostly the same and these systems seem equally suitable for doing real analysis. (They are nowhere near providing what could be called modern analysis though.) So the choice of one system over another will mostly depend on personal preferences. It should be remembered though that Mizar is based on a set-theoretical setting while all the other ones are type-based, so they might be more user-friendly. Note also that the Coq standard library for real numbers has not evolved much since its inception, so it is a bit outdated now; formalizations for PVS, HOL4, HOL Light, Isabelle/HOL, and ProofPower-HOL, have more closely tracked the evolutions of the underlying system. With respect to automation, PVS, HOL Light, Isabelle/HOL, HOL4, and Coq (standard library), are of similar strength: they have powerful procedures for arithmetic, but such procedures are somehow lacking when it comes to analysis. Finally, except for Coq, all the standard libraries we have surveyed provide a formalization of complex numbers, which might be of importance depending on the kind of analysis development the user wants to tackle. In the course of this survey, we encountered a few general issues that are worth reporting, as users are likely to stumble upon them. First of all, some standard libraries are in most parts poorly documented and one has to dive into the code of these systems to have a grasp of their extent. This may also have caused us to miss some hidden features of some systems. In particular, one can regret that, in this day and age, so few libraries have some browsable content online, i.e. an easy way to navigate from theorem statements to concept definitions without relying on dedicated tools. More importantly, it appears that some formalizations were developed in isolation, without any concern for the applications that might be built upon them later. As a consequence, while elegant, some developments might prove difficult to use in practice, due to some missing lemmas or the lack of specific methods of automation. A lesson for the future would be that applications should drive the development of formalizations and libraries, rather than the opposite. Yet developers should strive to keep some homogeneity and consistency in their formalizations, e.g. naming. In this survey, we have restricted ourselves to a small set of systems and libraries and are far from exhaustive. One can find numerous other developments formalizing real numbers out there. For instance,  and  provide formalizations for Nuprl.  shows how to complete metric spaces in LEGO, and thus how to build the real numbers from the set of rational numbers. BIB004 formalize real numbers in Coq as infinite stream of digits in {−1, 0, 1}. Using Coq too, Cohen (2012) presents a formalization of algebraic numbers. There are also works that extend the libraries presented in this survey. For instance, BIB002 formalize the O notation in Isabelle/HOL. BIB003 defines the Lebesgue integral and uses it for reasoning on probabilistic algorithms in Isabelle/HOL.  develops a theory of topology in PVS. BIB005 combine Coq's standard library with computable reals defined as infinite streams. BIB008 extend Coq's standard library to simplify differentiation and integration. To conclude this survey, we mention some large formal developments that were built thanks to the systems we presented. First, there are all the formalizations related to the verification of floating-point programs. Since floating-point arithmetic is used in practice as an approximation of real arithmetic, formal verification ends up relying on the latter. Most of the works have been performed with HOL Light, e.g. BIB001 , and Coq, e.g. BIB006 . There have also been some developments in ACL2, e.g.  , but it should be noted that they took great care to avoid irrational numbers and thus used plain ACL2 only. Another kind of application is the study of ordinary or partial differential equations. For ordinary differential equations, proofs about one-step methods and the Euler method have been done in Isabelle/HOL with an executable specification BIB009 . Still for ordinary differential equations, a computable Picard operator has been proved in C-CoRN/MathClasses  . Regarding partial differential equations, a major development about the numerical resolution of the wave equation was done in standard Coq BIB007 . Possibly one of the largest developments based on real analysis is the Flyspeck project; this is a HOL Light formalization of the theorem about dense sphere packings (Hales 2012, Solovyev and BIB011 ). Finally, one should note all the PVS works on verifying critical systems for avionics, e.g. BIB010 .