Abstract. This talk will start with a demonstration of the GEOTHER environment. We will use live examples to show how geometric theorems may be specified, manipulated, and proved automatically. The inherent difficulties of performing these tasks correctly lead to the foundational problem of geometry software design. We will explain how this problem is addressed in our GOOL project, which focuses on the design and implementation of a geometric-object-oriented language for symbolic geometric computing and reasoning. One of the main purposes of developing this language or system is for geometry education.