[FOM] Automatic theorem proving in trigonometry and synthetic geometry
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.
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
>> the fact that CDE = 20 degrees, do I have to rely on human ingenuity
>> is there a program that will find such a proof for me? Related
>> 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
>> 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.
> FOM mailing list
> FOM at cs.nyu.edu
More information about the FOM