Formalizing complex plane geometry. (English) Zbl 1330.68264

Summary: Deep connections between complex numbers and geometry had been well known and carefully studied centuries ago. Fundamental objects that are investigated are the complex plane (usually extended by a single infinite point), its objects (points, lines and circles), and groups of transformations that act on them (e.g., inversions and Möbius transformations). In this paper, we treat the geometry of complex numbers formally and present a fully mechanically verified development within the theorem prover Isabelle/HOL. Apart from applications in formalizing mathematics and in education, this work serves as a ground for formally investigating various non-Euclidean geometries and their intimate connections. We discuss different approaches to formalization and discuss the major advantages of the more algebraically oriented approach.


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
51B10 Möbius geometries
Full Text: DOI


[1] Barthe, G; Capretta, V; Pons, O, Setoids in type theory, J. Funct. Program., 13, 261-293, (2003) · Zbl 1060.03030
[2] Cohen, C.: Pragmatic quotient types in Coq. In: Sandrine, B., Christine, P.-M., Pichardie, D. (eds.) Interactive Theorem Proving, vol. 7998 of Lecture Notes in Computer Science, pp 213-228. Springer Berlin Heidelberg (2013) · Zbl 1317.68207
[3] Dehlinger, C., Dufourd, J.-F., Schreck, P.: Higher-Order Intuitionistic Formalization and Proofs in Hilberts Elementary Geometry. In: Automated Deduction in Geometry, vol. 2061 of Lecture Notes in Computer Science. Springer (2001) · Zbl 0985.68078
[4] Duprat, J.: Constructors: a ruler and a pair of compasses TYPES 2002 (2002)
[5] Génevaux, J.-D., Narboux, J., Schreck, P.: Formalization of Wu’s simple method in Coq. In: CPP, vol. 7086 of Lecture Notes in Computer Science. Springer (2011) · Zbl 1350.68234
[6] Geuvers, H., Wiedijk, F., Zwanenburg, J.: A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. In: Types for Proofs and Programs, vol. 2277 of Lecture Notes in Computer Science. Springer (2002) · Zbl 1054.03041
[7] Grégoire, B., Pottier, L., Théry, L.: Proof certificates for algebra and their application to automatic geometry theorem proving. In: Automated Deduction in Geometry, vol. 6301 of Lecture Notes in Computer Science. Springer (2008) · Zbl 1302.68242
[8] Guilhot, F.: Formalisation en coq et visualisation d’un cours de géométrie pour le lycée. Tech. et Sci. Informatiques 24(9) (2005)
[9] Haftmann, F., Wenzel, M.: Constructive type classes in isabelle. In: Types for Proofs and Programs, vol. 4502 of Lecture Notes in Computer Science, pp 160-174. Springer Berlin Heidelberg (2007) · Zbl 1178.68529
[10] Harrison, J.: A HOL Theory of Euclidean Space. In: TPHOLs, vol. 3603 of Lecture Notes in Computer Science. Springer (2005) · Zbl 1152.68520
[11] Harrison, J.: Without loss of generality.. In: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009, vol. 5674 of LNCS, Munich. Springer-Verlag, Germany (2009) · Zbl 1252.68254
[12] Harrison, J.: The HOL light theory of euclidean space. J. Autom. Reason. 50(2) (2013) · Zbl 1260.68373
[13] Hilbert, D., Townsend, E.J.: The Foundations Of Geometry. Kessinger Publishing (2006)
[14] Hille, E.: Analytic Function Theory. AMS Chelsea Publishing. American Mathematical Society (1973) · Zbl 0273.30002
[15] Huffman, B., Kunčar, O.: Lifting and Transfer A Modular Design for Quotients in Isabelle/HOL Certified Programs and Proofs, vol. 8307 of LNCS. Springer International Publishing (2013) · Zbl 1426.68284
[16] Janičić, P., Narboux, J., Quaresma, P.: The area method. J. Autom. Reason. 48(4) (2012) · Zbl 1242.68281
[17] Kahn, G.: Constructive geometry according to Jan von Plato. Coq contribution, Coq V5.10 (1995)
[18] Kaliszyk, C., Urban, C.: Quotients revisited for Isabelle/HOL. In: Proceedings of the 2011 ACM Symposium on Applied Computing, SAC ’11, pp 1639-1644, New York, NY USA ACM (2011)
[19] Magaud, N., Narboux, J., Schreck, P.: Formalizing Projective Plane geometry in Coq. In: Automated Deduction in Geometry, vol. 6301 of Lecture Notes in Computer Science. Springer (2011) · Zbl 1302.68246
[20] McKenzie Makarios, T.J.: A mechanical verification of the independence of Tarski’s Euclidean axiom Master’s thesis. Victoria University of Wellington (2012)
[21] Marić, F., Petrović, D.: Formalizing analytic geometries , Automated Deduction in Geometry (2012)
[22] Marić, F., Petrović, I., Petrović, D., Janičić, P.: Formalization and implementation of algebraic methods in geometry. In: THedu, vol. 79 of EPTCS (2011)
[23] Meikle, L., Fleuriot, J.: Formalizing Hilberts Grundlagen in Isabelle/Isar. In: Theorem Proving in Higher Order Logics, vol. 2758 of Lecture Notes in Computer Science. Springer (2003) · Zbl 1279.68291
[24] Milewski, R.: Fundamental theorem of algebra. Formalized Mathematics 9(3) (2001) · Zbl 0987.03041
[25] Narboux, J.: Mechanical Theorem Proving in Tarski’s Geometry. In: Automated Deduction in Geometry, vol. 4869 of Lecture Notes in Computer Science. Springer (2007) · Zbl 1195.03019
[26] Needham, T.: Visual Complex Analysis. Oxford University Press (1998) · Zbl 0893.30001
[27] Nipkow, T., Lawrence, C.P., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic vol. 2283 of LNCS. Springer (2002) · Zbl 0994.68131
[28] Penrose, R., Rindler, W.: Spinors and Space-Time Cambridge Monographs on Mathematical Physics. Cambridge University Press (1987)
[29] Schwabhäuser, W., Szmielew, W., Tarski, A., Beeson, M.: Metamathematische Methoden in der Geometrie. Springer Verlag (1983) · Zbl 0564.51001
[30] Schwerdtfeger, H.: Geometry of Complex Numbers Dover Books on Mathematics. Dover Publications (1979)
[31] Scott, P.: Mechanising Hilberts Foundations of Geometry in Isabelle. University of Edinburgh, Master’s thesis (2008)
[32] Sternagel, C., Thiemann, R.: Executable matrix operations on matrices of arbitrary dimensions Archive of Formal Proofs (2010). Formal proof development. http://afp.sf.net/entries/Matrix.shtml
[33] von Plato, J.: The axioms of constructive geometry. Ann. Pure Appl. Logic 76(2) (1995) · Zbl 0836.03034
[34] Wenzel M.: Isabelle/Isar — a generic framework for human-readable proof documents. In: From Insight to Proof — Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric vol. 10(23) University of Bialystok (2007)
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.