GeoGebra is an open-source educational mathematics software tool, with millions of users worldwide. It has a number of features (integration of computer algebra, dynamic geometry, spreadsheet, etc.), primarily focused on facilitating student experiments, and not on formal reasoning. Since including automated deduction tools in GeoGebra could bring a whole new range of teaching and learning scenarios, and since automated theorem proving and discovery in geometry has reached a rather mature stage, we embarked on a project of incorporating and testing a number of different automated provers for geometry in GeoGebra. In this paper, we present the current achievements and status of this project, and discuss various relevant challenges that this project raises in the educational, mathematical and software contexts. We will describe, first, the recent and forthcoming changes demanded by our project, regarding the implementation and the user interface of GeoGebra. Then we present our vision of the educational scenarios that could be supported by automated reasoning features, and how teachers and students could benefit from the present work. In fact, current performance of GeoGebra, extended with automated deduction tools, is already very promising—many complex theorems can be proved in less than 1 second. Thus, we believe that many new and exciting ways of using GeoGebra in the classroom are on their way.

The automatic determination of geometric loci is an important issue in Dynamic Geometry. In Dynamic Geometry systems, it is often the case that locus determination is purely graphical, producing an output that is not robust enough and not reusable by the given software. Parts of the true locus may be missing, and extraneous objects can be appended to it as side products of the locus determination process. In this paper, we propose a new method for the computation, in dynamic geometry, of a locus defined by algebraic conditions. It provides an analytic, exact description of the sought locus, making possible a subsequent precise manipulation of this object by the system. Moreover, a complete taxonomy, cataloging the potentially different kinds of geometric objects arising from the locus computation procedure, is introduced, allowing to easily discriminate these objects as either extraneous or as pertaining to the sought locus. Our technique takes profit of the recently developed GröbnerCover algorithm. The taxonomy introduced can be generalized to higher dimensions, but we focus on 2-dimensional loci for classical reasons. The proposed method is illustrated through a web-based application prototype, showing that it has reached enough maturity as to be considered a practical option to be included in the next generation of dynamic geometry environments

We review the behavior of some popular dynamic geometry software when computing envelopes, relating the diverse methods implemented in these programs with the various definitions of envelope. Special attention is given to the new GeoGebra 5.0 version, that incorporates a mathematically rigorous approach for envelope computations. Furthermore, a discussion on the role, in this context, of the cooperation between GeoGebra and a recent parametric polynomial solving algorithm is detailed. This approach seems to yield accurate results, allowing for the first time sound computations of envelopes of families of plane curves in interactive environments.