Automated geometric theorem-proving using synthetic methods

Question

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.

Answer 1

(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.)

Answer 2

There were some implementations in the 1950s and later, but the search space explosion is the main issue (as said above).

You can find more information in:

Shang-Ching Chou and Xiao-Shan Gao and Jing-Zhong Zhang. Machine Proofs in Geometry, World Scientific 1994.

Shang-Ching Chou and Xiao-Shan Gao. Automated reasoning in geometry, Handbook of Automated Reasoning, Elsevier 2001

Dongming Wang. Geometry machines: From AI to SMC. Artificial Intelligence and Symbolic Mathematical Computation, LNCS1138, Springer 1996.