> there is generally no formal geometric way to verify their correctness. There are formal models of synthetic (i.e. axiom-and-proof based) Euclidean geometry

> there is generally no formal geometric way to verify their correctness. There are formal models of synthetic (i.e. axiom-and-proof based) Euclidean geometry where proofs can in fact be verified. This is accomplished by rigorously defining the set of allowed "moves" in the proof and their semantics, much like one would define allowed steps in an algebraic computation.