## Formalization of the Poincaré disc model of hyperbolic geometry.(English)Zbl 07356967

Summary: We describe formalization of the Poincaré disc model of hyperbolic geometry within the Isabelle/HOL proof assistant. The model is defined within the complex projective line $$\mathbb{C}{}P^1$$ and is shown to satisfy Tarski’s axioms except for Euclid’s axiom – it is shown to satisfy it’s negation, and, moreover, to satisfy the existence of limiting parallels axiom.

### MSC:

 68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

### Keywords:

Poincaré model; Isabelle/HOL; formalization of geometry
Full Text: