Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
up vote 1 down vote accepted

For "geometric" angles ($180^{\circ}$ or less), two angles are equal precisely if their cosines are equal, and equality of cosines can be expressed algebraically. One can also handle in a similar way the notion of one angle being twice another, or three times another. As to the rest, it all depends on what you mean by the "etc." near the end of your question.

share|cite|improve this answer
'etc' means 'any angle relation mentioned in a proof in Euclid' – Mitch Apr 13 '11 at 21:28
so use the dot product is what you're getting at? – Mitch Apr 13 '11 at 21:28
@Mitch: Yes, dot product will do the job. One would have to go through Elements to see what angle relations are involved, but I am essentially certain that everything in Euclid's geometrical books would qualify. The only possible difficulties would arise in Book 10, where (in essence) there is an attempted classification of irrationals that arise in geometry. – André Nicolas Apr 13 '11 at 21:37

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.