[FOM] Automatic theorem proving in trigonometry and synthetic geometry

[Andrej Bauer]

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

This sort of trigonometric identities falls under "simplification" rather than "proving".
For example, Mathematica confirms your identity:

In[10]:= Tan[50 Degree] == Tan[20 Degree]/(1 - 4 Sin[10 Degree]) // FullSimplify
Out[10]= True

We did not obtain a proof but rather a confirmation that Mathematica thinks the identity holds.
The execution of the underlying simplification alogirthm is the proof of the identity (together with a proof of correctness of the algorithm). The execution could certainly be presented in a human-readable "proof by calculation", if anybody cared. Or you might give in and just trust the machine :-)

If you're not impressed yet, here's another one:

In[20]:= Pi/4 == 5*ArcTan[1/13]+5*ArcTan[1/21]+2*ArcTan[1/31]+2*ArcTan[1/43]+3*ArcTan[1/57] // FullSimplify
Out[20]= True

I don't know anything about finding a synthetic proof of the original geometry problem. It would be nice to have a general way of going from the (proof of) trigonometric identity to the (proof of) corresponding geometry problem. Then we'd have an infinite source of competition-level geometry problems.

Andrej