Towards the Automatic Discovery of Theorems in GeoGebra

Considerable attention and efforts have been given to the implementation of automatic reasoning tools in interactive geometric environments. Nevertheless, the main goal in such works focused on theorem proving, cf. Java Geometry Expert or GeoGebra. A related issue, automatic discovery, remains almost unexplored in the field of dynamic geometry software. This extended abstract sketches our initial results towards the incorporation into GeoGebra, a worldwide spread software with tenths of millions of users, of automatic discovery abilities. As a first result, currently available in the official version, we report on a new command allowing the automatic discovery of loci of points in diagrams. Besides the standard mover-tracer locus finding, the approach also deals with loci constrained by implicit conditions. Hence, our proposal successfully automates a kind of bound dragging in dynamic geometry, the 'dummy locus dragging'. In this way, the cycle of conjecturing-checking-proving will be accessible for general learners in elementary geometry.