Software for solving geometry questions

Question

When I used to compete in Olympiad Competitions back in high school, a decent number of the easier geometry questions were solvable by what we called a geometry bash. Basically, you'd label every angle in the diagram with the variable then use a limited set of basic geometry operations to find relations between the elements, eliminate equations and then you'd eventually get the result. It seems like the kind of thing you could program a computer to do. So, I'm curious, does there exist any software to do this? I know there is lots of software for solving equations, but is there anything that lets you actually input a geometry problem without manually converting to equations? I'm not looking for anything too advance, even seeing just an attempt would be interesting. If there is anything decent, I think it'd be rather interesting to run the results on various competitions and see how many of the questions it solves.

Answer 1

This is just a special case of automated theorem proving. A nice thing is some geometry problem can indeed be solved by an algorithm.

There are theories show such system can be realized algorithmically. I don't know if anyone have really wrote the program to do it. JGEX seems to do that.

A mechanical geometry proof technique was popularized in China by Jingzhong Zhang. He first introduced it as a way for machines to solve geometric problems relating the proportions between areas, lengths or angles. Then some Olympiad people I know start using it to bash that kind of problem. I don't know what the name is in English, but a literal translation of the method is "point removal method". Although it's not exactly same as what you are talking about, because "input a geometry problem" requires you to provide the construction of the problem from a straight edge and a compass, which is almost like "manually converting to equations".

the basic idea:

1. Construct the original problem by compass and straightedge, make a list of every constructed point ordered by the order of construction, let it be L. Record which points are used in the construction of every point.(Only the points used to construct point P are used in the substitution steps 3 and 4)

2. Translate the theorem into a equivalent form. Usually a/b = 1, where a and b are functions of length and area of certain segments or triangles. Let's call this equation E.

3. Let P be the last point of L. For every P appears in E, substitute it with another relation using other points from L(P itself is also allowed), usually if we are proving about lengths, we might use area. A list of possible operations are required for this step. It can branches off as a proof tree when the program decide to use different substitutions.

4. Do another substitution that eliminates the point P. For example, if in the step before, we substitute length to area, then we want to find something involve the length.

5. Do 3 to 4 over and over until we have 1=1

An example:

Angle bisector theorem

Given: $AD$ is the angle bisector of $\angle BAC$ of triangle $\triangle ABC$. Let $XYZ$ be the area of triangle $\triangle XYZ$, and $XY$ be the length of segment $XY$.

Prove: $\frac{AB}{AC} = \frac{BD}{DC}$

Proof:

1. First construct $ABC$. Then construct $AD$. The points in the list $L$ are $A,B,C,D$.

2. The equivalent equation to the theorem is $\frac{AB}{AC} \frac{DC}{BD} = 1$

3. $\frac{AB}{AC} \frac{DC}{BD} = \frac{AB}{AC} \frac{ACD}{ABD}$ (substitute length with area)

4. $=\frac{AB}{AC} \frac{\frac{1}{2} AC\cdot AD \sin \angle CAD}{\frac{1}{2} AB\cdot AD \sin \angle BAD}$, this step successfully remove point $D$ by cancellation.

5. $=\frac{AB}{AC} \frac{AC}{AB} =1$

This is only a non-formal explanation of how such automated system would work. I think the following book from Zhang will tell you more about it: Machine proofs in geometry: automated production of readable proofs for geometry theorems. I did not read the book, but the description of it seems like what you are seeking. A few paper by Zhang and his colleague can be found in the JGEX's website. The JGEX documentation on it's automated theorem prover is also a great resource.

Answer 2

You might be interested in Doron Zeilberger's website. He has a page entitled "Plane Geometry: An Elementary Textbook (Circa 2050)" where he envisioned a world in which computers can derive all of plane geometry without human intervention or interference. The accompanying Maple package proves many statements by computer.

The page exists at http://www.math.rutgers.edu/~zeilberg/PG/gt.html.