Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Elementary Functions <s> 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. <s> BIB001 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> Elementary Functions <s> 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. <s> BIB002
Finally, the notions formalized above are used to define some elementary functions: exponential, logarithm, trigonometric functions, and their inverses. Most provers provide all these functions but their definitions present some variations, e.g. by power series or integrals. 4.4.1. Using power series As written above, series and power series are generally defined to formalize exponential, sine, and cosine. Coq's standard library  , C-CoRN, HOL4 BIB001 , the sub-library about series of PVS Shankar 2003, Gottliebsen 2000) , the PVS constructive reals, and ACL2(r) BIB002 , use the following power series to define them: In MathClasses, exp, sin, and arctan, are defined using power series (O'Connor 2008,  and the other trigonometric functions, such as cos or ln are defined from these three. Then π is defined from arctan using a Machin-like formula, as in PVS' constructive reals. HOL Light defines the exponential function with power series over complex numbers and then defines the exponential on real numbers and the trigonometric functions from it. Mizar uses the same approach for defining the trigonometric functions, but not for the exponential on real numbers (cf. Section 4.4.4). These two formalizations are the only ones to define power series on complex numbers.