Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Introduction <s> 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. <s> BIB001 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Introduction <s> 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 <s> BIB002
Rational numbers have been used for millennia to compute areas, taxes, etc. Calculus has been developed in the 18th century and now all students are used to knowing and computing with 3, 1 7 , √ 13, exp(1), and π. Calculus and computations are even seen as a way to select the assumed "best" students. Real analysis is indeed a good test case for students: knowing definitions and theorems, they are assessed for reasoning and correctly applying theorems. When it comes to proof assistants, the situation is the opposite: they are designed for reasoning, but are to be assessed for definitions and theorems about real analysis. Our objective is similar to that of  : he compared seventeen provers by showing how to prove that √ 2 is irrational. (Note that this lemma can be stated using only integers and thus does not tell much about support for real analysis.) The appeal of that work is that it collects proof written by power users of those formal systems. BIB002 then compared libraries: that latter work presents statistics about the whole standard libraries of some provers, but it does not look at the actual definitions and theorems. Our goal is to compare the formal systems on their abilities to prove mathematical properties of real analysis and how much help they provide to the user. The aim of this survey is to give the reader an overview of the available systems, their libraries and tools for formal reasoning about real analysis. This comparison is needed since many different design choices have been made. That way, a user accustomed to formal methods may choose the most appropriate system for proving a real analysis result. No such survey has been written before, and even the available literature is sometimes insufficient to compare libraries and definitions. Formal proof assistants are quite recent in computer science history: the first influential system was AutoMath in 1967, though there were some earlier works BIB001 . Then came Boyer- Moore (1971) , LCF (1972) , Mizar (1973) , and many more systems. Real number formalizations soon followed  and research is ongoing. Our goal here is not to survey all the provers. For the sake of significance, we restrict ourselves to systems that stood the test of time. Moreover they have to come with a standard library for real arithmetic. They also have to provide support for real analysis, and not just a construction of real numbers. The standard libraries we have picked out are those of Mizar, PVS, HOL4, HOL Light, Isabelle/HOL, and Coq. We have also accounted for large developments that play a role similar to standard libraries: ACL2(r) for ACL2, C-CoRN/MathClasses for Coq, and the NASA PVS library. Another choice of ours is to focus on real analysis and to ignore probabilities and most of measure theory. This survey is organized as follows: Section 2 describes the various proof assistants and libraries we will focus on. Section 3 shows the various formalizations of the set R of real numbers. Section 4 outlines the choices they made for the usual definitions found in real analysis. Available methods of automation are presented in Section 5.