  We describe our ongoing project of formalization of algebraic methods for
geometry theorem proving (Wu's method and the Groebner bases method), their
implementation and integration in educational tools. The project includes
formal verification of the algebraic methods within Isabelle/HOL proof
assistant and development of a new, open-source Java implementation of the
algebraic methods. The project should fill-in some gaps still existing in this
area (e.g., the lack of formal links between algebraic methods and synthetic
geometry and the lack of self-contained implementations of algebraic methods
suitable for integration with dynamic geometry tools) and should enable new
applications of theorem proving in education.
