In Is it possible to solve any Euclidean geometry problem using a computer? I claimed that one can convert the statement of a theorem in Euclid into multivariate polynomials such that Groebner basis completion would supply an 'automated' proof:
- an arbitrary point can be represented by two variables $(x,y)$
- a line by two points $(x_1,y_1),(x_2,y_2)$
- a point $(x_3,y_3)$ on a line $(x_1,y_1),(x_2,y_2)$ by $(y3-y_1)(x_2-x_1) = (x_3-x_1)(y_2-y_1)$
- a point on a circle with radius $d$ by $(x_1-x_2)^2 + (y_1-y_2)^2 = d^2$. (and of course the distance itself might be from another definition of a circle.
I left out the additional translation of the 'angle' concept. A large part of Euclid involves use of angles (for example, the angles opposite equal sides of a triangle are equal, or the sum of the interior angles of a triangle is $\pi$).
It should be straightforward to translate an angle into a statement about points. Three points in order somehow represent an angle at the middle point. But I can't figure out how to show that two angles are equal by converting them to polynomials, or show that one angle is half another, etc.
Any ideas?