[FOM] Automatic theorem proving in trigonometry and synthetic geometry

[Jeremy Clark]

On Jul 21, 2004, at 4:55 pm, Timothy Y. Chow wrote:

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

Having thought further, I now see that the trigonometric case that I 
have been ham-fistedly blundering towards generalises to the geometric 
case: so the answer is, yes: your geometry problem *can* be blindly fed 
into a computer, converted into a purely algebraic statement about 
polynomials over Z, and then solved by usual factorisation algorithms. 
There's nothing "state of the art" about it: I think Gauss would have 
been able to answer your question, though my knowledge of maths history 
is shaky. The method is essentially the same as the proof that points 
constructed by ruler and compass belong to certain extensions of Q, as 
given in e.g. Garling's "A Course in Galois Theory".

Jeremy
(with apologies for needless multiple posts)


>