GeoGebra Automated Reasoning Tools is a module of the dynamic mathematics software GeoGebra that combines dynamic geometry and computer algebra to exploit modern methods in formalizing and proving conjectures based on algebraic geometry. In this paper we address some unequivocal results on this novel tool, and also give a list of challenges on the educational use as well.
GeoGebra Automated Reasoning Tools (ART) is an embedded module of the dynamic mathematics software GeoGebra (Fig. 1, available at www.geogebra.org), a computer program that is used by millions of students and teachers worldwide in education. Development of GeoGebra ART has started in the beginning of the 2010's, but former theoretical and experimental foundations have been established much before that, with roots in Chou's revolutionary book [Cho88], and former authors including Wu, Buchberger, Tarski and Hilbert.
In a nutshell, GeoGebra ART exploits advantages of planar dynamic geometry visualizations, and adds symbolic checks of user-initiated conjectures in an intuitive way. For example, GeoGebra ART provides a symbolic Relation tool that is able to perform a symbolic check of numerical perceptions of typical geometric properties between objects, including parallelism, perpendicularity, equality, concurrency, collinearity, concyclicity and others. (See [KRV17] for a tutorial.)
Also, some commands have been introduced that are to be typed by the user, but they provide an easy syntax to make it possible to sketch up conjectures and obtain their automated proofs in a very quick way. GeoGebra ART has commands LocusEquation and Envelope to obtain dynamic locus curves based on pure symbolic computations.
Advantages and challenges Since GeoGebra ART is a new tool, we do not have enough feedback to con rm or confute our con dence and doubt concerning its novel use cases.
On the one hand, several collections of examples already exist that demonstrate the strength of GeoGebra ART. In particular, it provides obtaining new conjectures with implicit proofs, but this process heavily relies on the user's initiative. For example, by drawing a triangle and creating its altitudes, the software waits for user interaction to get the altitudes compared, and only after the user's wish there will be a comparison started. Then, after a positive result (that is, the altitudes are concurrent in a particular case) the software o ers performing a symbolic check to investigate the general case as well (Fig. 2).
Also, when obtaining implicit locus equations, classi cation of the computed algebraic curve is a task that is left to the user. For instance, by issuing the command LocusEquation(a==b,C) in an arbitrary triangle having vertices A, B and C, and sides a, b and c, respectively, a visually straight line will be obtained in the Graphics View with a linear equation shown in the Algebra View (Fig. 3)1. It is, however, not a trivial question if a linear equation always depicts a straight line and vice versa, at least not in secondary education. In fact, the user needs to drag points A, B and C to collect more experiences to conclude a conjecture that the locus equation is 1The issued command symbolically solves the question Which points C in the plane have the property that a = b, given that a = jBCj and b = jACj? |here A and B are xed points and C is to be found. Actually, the solution of this question is the perpendicular bisector of AB, if A 6= B; in this latter case the solution is the whole plane, that is, 0 = 0. always a straight line, and it has a corresponding equation of the form
for certain ; ; 2 R.
In our opinion, therefore, GeoGebra ART is a tool that rather supports mathematical thinking than simply unfolds some mathematical truths that are maybe interesting for its programmers and the teacher users, but completely unconcerned for the students who use it.
On the other hand, some risks can be identi ed. One of them is a kind of mathematical issue: in some extremal circumstances numerical checks lead to false results. For example, Fig. 4 shows a strange situation where the lines AB and CD are not reported to be perpendicular anymore after zooming out from the initial view (Fig. 5). Here the numerically evaluated value of g, which is de ned as AB ? CD, can be false in several positions of A and B. Since D is de ned to be the orthocenter of triangle ABC as the intersection of altitudes through A and B, g should be true in theory, but the numerical check is erroneous (see also [Kov15, p. 33] and https://dev.geogebra.org/trac/attachment/ticket/1044/miguels_prover.ggb). In such cases the internal low-level command Prove can be issued to double-check the truth, in fact, symbolically (Fig. 6).
The other risk, in our opinion, is very similar to the very well-known risk of utilization of modern tools, the Shift-Enter problem, identi ed by Vajda2 in the beginning of the 2000's during an exam where the solution of a maths question was disclosed by a student with the short answer \just use Shift-Enter"3. In particular, when obtaining a positive answer on collinearity of the altitudes, the student may have the feeling that \it is the end of story", the computer did its best and no further steps could be done. On the contrary, a good student should either nd an elegant way of reasoning|note that the computer does not show the proof in GeoGebra ART to avoid thousands of atomic steps that hide the essence of the mathematical content!|, or nd additional conjectures that are similar to the one being found. For example, a good student should then continue with comparing the medians or the bisectors of a triangle.
For some non-trivial applications of GeoGebra ART, including clever questions of some hypothetical \good students", we refer to [Kov18] that highlights Buchberger's framework on the creativity spiral approach [Buc98]. [KRV17] Kovacs, Z., Recio, T. and Velez, M. P.: GeoGebra Automated Reasoning Tools. A Tutorial. 2017.
Retrieved from https://github.com/kovzol/gg-art-doc. [Kov15] Kovacs, Z.: Computer Based Conjectures and Proofs in Teaching Euclidean Geometry. PhD thesis,
Johannes Kepler University, Linz, Austria. 2015. [Kar14] Karacal, E.: ME 443 Mathematica for Engineers. Basic calculations. 2014. Retrieved from https: //www.slideshare.net/garacaloglu/me-443-3-basic-calculations. [Kov18] Kovacs, Z. Automated reasoning tools in GeoGebra: A new approach for experiments in planar geometry. South Bohemia Mathematical Letters 25(1). 2018.