[FOM] Automatic theorem proving in trigonometry and synthetic geometry

[Timothy Y. Chow]

I flew United Airlines this past weekend and there was an IQ test in their
"Hemispheres" magazine with eleven easy problems plus one high-school
geometry problem that was much harder than anything one would expect to 
see in such a publication.  Essentially, the problem was this:

   Let ABC be a triangle with a point D on side AB and a point E on
   side AC.  We are given the following angles (in degrees):

   ABE = 20;  EBC = 60;  ACD = 10;  DCB = 70.

   Problem: What is angle CDE in degrees?

The answer is 20 degrees, and can be derived by a variety of trigonometric
means.  Now, given that the answer is so simple, one might expect there to
be a simple "synthetic proof."  Although such a proof surely exists (I 
don't happen to know one, by the way), it is not going to be quite as 
simple as one might naively expect, because this problem belongs to the
notoriously tricky genre of "adventitious angle" problems.  To put it 
another way, if the four given angles of the problem are replaced by
variables w, x, y, and z, then the desired angle will not, in general,
be a rational multiple of pi even if w, x, y, and z are.  The particular
angles in the problem, despite appearances, are not arbitrary but are
carefully chosen.

The reason I bring this up on FOM is that I am wondering whether the state
of the art in automated theorem proving is such that this kind of problem
can be (more-or-less blindly) fed to a program that will solve it.  I
should clarify that I am *not* asking about algorithms that are
specifically tailored for adventitious angle problems and nothing else,
but about general-purpose programs for solving problems in "high-school
geometry and trigonometry."

Another way to pose my question is this.  If I want a synthetic proof of
the fact that CDE = 20 degrees, do I have to rely on human ingenuity or
is there a program that will find such a proof for me?  Related question:
If I decide to tackle the problem by hand using trigonometry and find 
myself needing to prove (say) that tan(50) = tan(20)/(1-4sin(10)), do I
have to think or can a machine generate the proof for me?

Tim