Tarski Geometry Axioms
William Richter, Adam Grabowski, Jesse Alama (2014)
Formalized Mathematics
Similarity:
This is the translation of the Mizar article containing readable Mizar proofs of some axiomatic geometry theorems formulated by the great Polish mathematician Alfred Tarski [8], and we hope to continue this work. The article is an extension and upgrading of the source code written by the first author with the help of miz3 tool; his primary goal was to use proof checkers to help teach rigorous axiomatic geometry in high school using Hilbert’s axioms. This is largely a Mizar port of Julien...