Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> HOL Light <s> 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. <s> BIB001 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> HOL Light <s> 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. <s> BIB002 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> HOL Light <s> 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. <s> BIB003 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> HOL Light <s> 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. <s> BIB004 </s> Formalization of Real Analysis: A Survey of Proof Assistants and Libraries <s> HOL Light <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> BIB005
 ¶ is a formal system based on classical higher-order logic with axioms of infinity, extensionality, and choice in the form of Hilbert's operator BIB003 ). It follows the LCF approach with a small kernel written in OCaml BIB002 . The basic inference rules may be composed and methods of automation are available. The user may also program its own methods of automation. HOL Light was almost entirely written by Harrison. However, it builds on earlier versions of HOL, notably the original work by BIB001 and the improved implementation by Slind. Its formalization of real analysis originated in HOL88  ) and large parts of it were ported to HOL Light, HOL4, and Isabelle/HOL. Motivated by the Flyspeck project BIB004 , the HOL Light library of real analysis was later generalized into a formalization of Euclidean spaces while keeping the same construction of real numbers BIB005 . This survey only covers this latter formalization. Details about the earlier formalization can be inferred from the description of the HOL4 library of real analysis as it has not diverged much. The real numbers of HOL Light are described in Section 3.2.1. In HOL Light  , DIFF CONV proves results about the derivative of expressions. It syntactically and repeatedly applies the rules for differentiating sums, differences, products, and quotients. It also knows about the derivatives of basic functions like x n and some elementary functions, and the user may augment this set of functions. The derivative may also be postulated by the system.