This question is about geometric theorem proving and is inspired by this Math.SE post. Currently, Euclidean-geometric theorem provers, as referred to in the post, use coordinate geometry to convert a geometry problem into a set of algebraic equations.

Why haven't people developed a theorem prover that uses synthetic reasoning ?

By 'synthetic' I mean reasoning from axioms. I feel that synthetic reasoning would be more insightful than solving a large number of equations; yet, am unsure about how well it yields to implementation. Can you offer more insight? What would be the benefits and drawbacks of such a prover?

Also,I felt that my question would be more appropriate here than on Math.SE.

This question is about geometric theorem proving and is inspired by this Math.SE post. Currently, Euclidean-geometric theorem provers, as referred to in the post, use coordinate geometry to convert a geometry problem into a set of algebraic equations.

Why haven't people developed a theorem prover that uses synthetic reasoning ?

By 'synthetic' I mean reasoning from axioms. I feel that synthetic reasoning would be more insightful than solving a large number of equations; yet, am unsure about how well it yields to implementation. Can you offer more insight? What would be the benefits and drawbacks of such a prover?

Also,I felt that my question would be more appropriate here than on Math.SE.