Automated geometric theorem-proving using synthetic methods
(Note: I don't know anything about geometric reasoning, so I'm shifting from my limited experience in automated theorem proving in another field. I think the fundamental issue is the same.)

Synthetic reasoning tends to blow up exponentially. Typically, after $n$ steps of reasoning, there are about $a^k$ ways to choose a next step for some $a \gt 1$. There might be some overlap because there are multiple ways to prove the same theorem, but you still end up with a really fast combinatorial explosion in practice.

Reasoning from the goal is typically a lot tamer, because you tend to try to deduce the goal from simpler premises. It's still impractical in all but rather constrained settings (e.g. some arithmetic or geometric theories).

Putting a geometric problem into equations sets a boundary on the problem. You have $p$ equations and $q$ unknowns, now go and solve. Since the problem is bounded, the search for a solution will not go on forever. Furthermore, this form is convenient for many shortcut tricks that allow for faster solving, because solving algebraic equations is a well-known problem.

This choice of method is not less insightful than synthetic reasoning. An algebraic solver can keep track of the reasoning steps that it uses, and produce a proof trace that explains why the purported solution is really a solution. (Not all solvers bother to keep a proof trace.) This proof trace can be expressed in terms of geometric axioms. Thus you can get the same amount of insight no matter how the proof was obtained. (Insight, or lack thereof: in synthetic reasoning, “and then you apply this lemma” doesn't tell you why this lemma rather than any other lemma.)