[FOM] Automatic theorem proving in trigonometry and synthetic geometry
Jeremy Clark
jclark at noos.fr
Thu Jul 22 02:29:15 EDT 2004
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
>
More information about the FOM
mailing list