[FOM] Automatic theorem proving in trigonometry and synthetic geometry

[Jeremy Clark]

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

Any identity involving a polynomial in sin's and cos's of rational 
multiples of pi, can be boiled down mechanically to a single polynomial 
in z = exp(i*pi/n). This polynomial can then be factorised, and the 
identity holds if and only if each factor divides the polynomial z^n-1. 
And all in polynomial time! (I think.) Eat your heart out mathematica.

Jeremy