Automated Geometry Theorem Proving
Summary
Automated Geometry Theorem Proving (AGTP) is an algebraic approach to (dis)proving geometric statements in such a way that it can be (mostly) fully automated. The main idea is to translate the given geometric properties to polynomials, where the variables are the coordinates of the given points, and look at the corresponding variety. One way (a first approach) to see if a certain property holds, is to see if its corresponding polynomial is contained in the vanishing ideal of the initial variety. A more complete approach is Wu's Method, which relies on the theorem behind ascending chains and pseudo-remainders.
To try out how far we can automate this approach, I have implemented the concept of AGTP in Python.