The HOL Light theory of Euclidean space

Journal of Automated Reasoning, vol. 50, pp. 173-190 (2013).

Abstract:

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.

PDF

Bibtex entry:

@ARTICLE{harrison-pnt,
        author          = "John Harrison",
        title           = "The {HOL} {L}ight theory of Euclidean space",
        journal         = "Journal of Automated Reasoning",
        year            = 2013,
        volume          = 50,
        pages           = "173--190"}