Formalization of Tarski axioms of Euclidean geometry

Notes

You can use hammer with import Hammer. To debug use

set_option auto.tptp true
set_option trace.auto.tptp.result true

Let hammer do its thing and take its output to duper as

duper [*, seg_constr, eqd_trans] {preprocessing := full}

It is almost okay to leave duper, ideally you should also convert duper proofs to native ones.