Tarski's Geometry Modelled in Mizar Computerized Proof Assistant

In the paper, we discuss the formal approach to Tarski geometry axioms modelled with the help of the Mizar computerized proof assistant system. Although our basic development was inspired by Julien Narboux's Coq pseudo-code and is dated hack to 2014, there are significant steps in the formalization of geometry done in the last decade of the previous century. Taking this into account, we will propose the reuse of existing results within this new framework (including Hilbert's axiomatic approach), with the ultimate future goal to encode the textbook Metamathematische Methoden in der Geometric by Schwabhauser, Szmielew and Tarski. We try however to go much further from the use of simple predicates in the direction of the use of structures with their inheritance, attributes as a tool of more human-friendly namespaces for axioms, and registrations of clusters to obtain more automation (with the possible use of external equational theorem provers like Otter/Prover9).