[FOM] Automatic theorem proving in trigonometry and synthetic geometry

[Jeremy Clark]

I posted a little too hastily. z should have been exp(i*2*pi/n), and 
the identity holds if and only if *one* of the factors divides *p_z*, 
the characteristic polynomial of z. (Which is a prime factor of z^n-1.) 
The point is that all the factorising etc. can be done over Z, or 
perhaps Z[i] - thanks to Gauss's lemma - and so is decidable.

Jeremy

On Jul 21, 2004, at 9:47 pm, Jeremy Clark wrote:

>>
>> 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
>
>
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>