This question is about geometric theorem proving and is inspired by this <a href="http://math.stackexchange.com/questions/31192/is-it-possible-to-solve-any-euclidean-geometry-problem-using-a-computer"> Math.SE </a> 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 <i>synthetic</i> 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.