Formalization, Automatization and Visualization of Hyperbolic Geometry

Abstract

In this talk we describe our experiences with the formalization, automation and visualization of non-Euclidean geometries.

We start with a formalization of the complex projective line CP(1) (also known as the extended complex plane), its objects (points and circlines) and transformations (Möbius transformations). An algebraic approach is used, where points are described with homogeneous coordinates, circlines are described with Hermitean matrices and Möbius transformations are described using regular matrices. We use the unit disk in CP(1) for the formalization of the Poincaré disk model of hyperbolic geometry and show that it satisfies all Tarski axioms of geometry (with the negated Euclidean axiom).

We also analyze the problem of automatic construction of triangles in absolute and hyperbolic geometry. For this purpose we adapt the software ArgoTriCS. For the visualization of the generated constructions we use ArgoDG: a lightweight JavaScript library for dynamic geometry.

Finally, we introduce the formalization of gyrogroups and gyrovector spaces introduced by Abraham Ungar, which is an alternative approach to formalize hyperbolic geometry inspired by Einstein's special theory of relativity.