The HOL Light theory of Euclidean space. (English) Zbl 1260.68373

Summary: 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.


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI


[1] Fontaine, P.: Techniques for verification of concurrent systems with invariants. Ph.D. thesis, Institut Montefiore, Université de Liège (2004)
[2] Geuvers, H., Wiedijk, F., Zwanenburg, J.: A constructive proof of the fundamental theorem of algebra without using the rationals. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) Types for Proofs and Programs, Proceedings of the International Workshop, TYPES 2000. Lecture Notes in Computer Science, vol. 2277, pp. 96–111. Springer (2001) · Zbl 1054.03041
[3] Hales, T.C.: Introduction to the Flyspeck project. In: Coquand, T., Lombardi, H., Roy, M.-F. (eds.) Mathematics, Algorithms, Proofs. Dagstuhl Seminar Proceedings, vol. 05021. Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany (2006)
[4] Hales, T.C.: The Jordan curve theorem, formally and informally. Am. Math. Mon. 114, 882–894 (2007) · Zbl 1137.03305
[5] Hales, T.C., Harrison, J., McLaughlin, S., Nipkow, T., Obua, S., Zumkeller, R.: A revision of the proof of the Kepler conjecture. Discrete Comput. Geom. 44, 1–34 (2010) · Zbl 1195.52004
[6] Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD’96), Lecture Notes in Computer Science, vol. 1166, pp. 265–269. Springer (1996)
[7] Harrison, J.: Theorem Proving with the Real Numbers. Springer (1998). Revised version of author’s Ph.D. thesis
[8] Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T. (eds.) Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005. Lecture Notes in Computer Science, vol. 3603, pp. 114–129. Springer, Oxford, UK (2005) · Zbl 1152.68520
[9] Harrison, J.: Formalizing basic complex analysis. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec. Studies in Logic, Grammar and Rhetoric, vol. 10(23), pp. 151–165. University of Białystok (2007)
[10] Harrison, J.: Without loss of generality. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009. Lecture Notes in Computer Science, vol. 5674, pp. 43–59. Springer, Munich, Germany (2009) · Zbl 1252.68254
[11] Hurd, J.: Integrating Gandalf and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs’99. Lecture Notes in Computer Science, vol. 1690, pp. 311–321. Springer, Nice, France (1999)
[12] Hurd, J.: Formal verification of probabilistic algorithms. Ph.D. thesis, University of Cambridge (2001)
[13] Jutting, L.S.v.B.: Checking Landau’s ”Grundlagen” in the AUTOMATH system. Ph.D. thesis, Eindhoven University of Technology (1977). Useful summary in Nederpelt, R.P., Geuvers, J.H., Vrijer, R.C.d. (eds.) Selected Papers on Automath. Studies in Logic and the Foundations of Mathematics, vol. 133, pp. 701–732. North-Holland (1994)
[14] Keller, C., Werner, B.: Importing HOL light into Coq. In: Kaufmann, M., Paulson, L.C. (eds.) First International Conference on Interactive Theorem Proving, ITP 2010. Lecture Notes in Computer Science, vol. 6172, pp. 307–322. Springer, Edinburgh, UK (2010) · Zbl 1291.68353
[15] Kuhn, H.W.: Some combinatorial lemmas in topology. IBM J. Res. Dev. 4, 518–524 (1960) · Zbl 0109.15603
[16] Milewski, R.: Fundamental theorem of algebra. J. Formal. Math. 12 (2000). http://mizar.org/JFM/Vol12/polynom5.html
[17] Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Ternovska, E., Schulz, S. (eds.) Proceedings of the 8th International Workshop on the Implementation of Logics, pp. 1–11 (2010)
[18] Solovay, R.M., Arthan, R., Harrison, J.: Some new results on decidability for elementary algebra and geometry. ArXiV preprint 0904.3482. Submitted to Ann. Pure Appl. Logic. Available at http://arxiv.org/abs/0904.3482 (2009)
[19] Sussmann, H.J.: Multidifferential calculus: chain rule, open mapping and transversal intersection theorems. In: Hager, W.W., Pardalos, P.M. (eds.) Optimal Control: Theory, Algorithms, and Applications, pp. 436–487. Kluwer (1998) · Zbl 0981.49013
[20] Webster, R.: Convexity. Oxford University Press (1995)
[21] Wiedijk, F.: Statistics on digital libraries of mathematics. In: Grabowski, A., Naumowicz, A. (eds.) Computer Reconstruction of the Body of Mathematics. Studies in Logic, Grammar and Rhetoric, vol. 18(31). University of Białystok (2009)
[22] Yee, L.-P., Výborný, R.: The Integral: An Easy Approach After Kurzweil and Henstock. Australian Mathematical Society Lecture Series. Cambridge University Press (2000) · Zbl 0941.26003
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.