[FOM] Automatic theorem proving in trigonometry and synthetic geometry
Jeremy Clark
jeremy.clark at wanadoo.fr
Wed Jul 21 15:47:40 EDT 2004
>
> 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
More information about the FOM
mailing list