Is there a formalization of absolute geometry? I am trying to formalize absolute geometry, and it means the following:
I want to express the axioms through of symbols only, and make the proofs by means of inference rules and definitions. I don't want words in my proofs, I only want symbols, every proof will be a complete proof.
But I am having many problems with this, so I thought that maybe someone has tried the same than me, and, Indeed, my question is related with that.
Is there a formalization of abslute geometry?
Now, If it's the case, where can I find it?
 A: Absolute geometry can be formalized using Hilbert's axioms without the parallel axiom.
A complete formalization of Euclidean geometry in the Coq proof assistant is given in [1], a thesis in which you will find further references. It covers Hilbert's axioms and Tarski's axioms and the relations between them. You might also be interested in [2], which makes use of the interactive theorem prover ELFE.
[1] P. Boutry, On the formalization of foundations of geometry, Thesis, Université de Strasbourg, France, 2018.
[2] M. Doré and K. Broda, Towards Intuitive Reasoning in Axiomatic Geometry, THedu@FLoC 2018: 38-55
Table of Contents of [1] (extract)
Part I. Foundations of Euclidean Geometry 9
Chapter I.1. Tarski’s System of Geometry: a Theory for Euclidean Geometry 13

*

*Formalization of Tarski’s Axioms 13

*Satisfiability of the Theory 17

*The Arithmetization of Tarski’s System of Geometry 20

Chapter I.2. Hilbert’s axioms: a Theory Mutually Interpretable with Tarski’s System of Geometry 25

*

*Formalization of Hilbert’s Axioms 25

*Proving that Tarski’s Axioms follow from Hilbert’s 31

Chapter I.3. Metatheorems about Tarski’s System of Geometry 37

*

*Independence of Euclid’s Parallel Postulate via Herbrand’s Theorem 37

*Towards the Decidability of Every First-Order Formula 43

Conclusion of Part I
