Automated Reasoning Tools with GeoGebra: What Are They? What Are They Good For?

Abstract

The popular dynamic mathematics program GeoGebra now includes tools for the mathematically rigorous proof and discovery of general statements on geometric figures. This chapter will, first, present the current state of development of these automated reasoning tools. Then the authors will reflect on the potential educational impact of these new features. The introduction of a new design for school tasks could serve to guide students toward inquiry, conjecture, and the discovery of geometric properties of a given figure. Other possible (future) educational applications of these tools will be discussed.

1 Introduction

We are immersed in the society of digitalization, automation, data science, and artificial intelligence. The interaction of this scenery with mathematics is twofold. On the one hand, mathematics is the hidden support for this whole technological panorama; on the other, personal computers provide digital tools that perform incredible calculations (including most of the tasks required in the current mathematics curriculum) or facilitate drawing dynamic graphs that help visualize mathematical objects. Yet, it seems that the current mathemathics education landscape does not respond to, or remains far from, what the new reality itself demands. “No mainstream school maths curriculum has yet been based on the (obvious) assumption that computers exist.” (Wolfram 2020, p. 4). This incoherent absence is perhaps one of the reasons for the current widespread debate within the educational community about what, how, and why to teach and learn mathematics, at all educational levels.

Digitalization brings to math education new tools that require a new curriculum, a new design of tasks, and a greater interaction with other disciplines (as in the STEAM approach). But, what is more important in this new context is the leading role of the student—with the help of digital tools—regarding his/her own learning process. For example, working through open-ended tasks, that can be defined as “...tasks where students are asked to explore objects and to discover and investigate their mathematical properties...” (Ulm 2011, p. 23)

In this new educational context, Dynamic Geometry Systems (DGS) can be considered as specifically appropriate, useful tools. Indeed, these software environments were, from their conception, meant mainly as a tool for fostering students’ ability regarding geometric visualization and experimentation. Nowadays, modern DGS have started to include features for automated reasoning that allows for the automatic and mathematically rigorous verification and discovery of geometric theorems Kovács et al. (2018), say a kind of “geometry calculator” for AI (“augmented intelligence”¹), that can improve the teaching and learning of reasoning and proof Sinclair et al. (2016) using an open-ended task methodology.

Thus, the popular dynamic mathematics program GeoGebra has always offered, as has any other Dynamic Geometry System, some remarkable possibilities to improve the construction and visual exploration of geometric objects. This is done by dragging the elements in a figure, thereby allowing the student to perceive the resulting changes and permanent relations by dragging the elements in a figure and, then, facilitating the student to perceive the resulting changes and the permanent relations. GeoGebra’s potential for problem solving, reasoning, and the influence of task design is analyzed in Olsson (2019), where the reader can find a revision of earlier research into the potential of dynamic software to support problem solving and reasoning.

Yet, more recently, since the computer algebra system Giac was embedded in GeoGebra Kovács and Parisse (2015), GeoGebra has been able to have implemented automated proving algorithms based on the algebraic approach described in Recio and Vélez (1999) and Kovács et al. (2019). The result is a collection of GeoGebra features and commands (the so-called Automated Reasoning Tools (ART)) that allow the rigorous mathematical verification (i.e., the Automatic Theorem Proving (ATP)) and the automatic discovery of general propositions about Euclidean geometry figures built by the user.

Although mathematics education experts have long been aware of the existence of dynamic geometry programs that offer, on an experimental basis and with a limited number of users, certain ATP features, the accessibility (as it is free of charge) and portability of GeoGebra; its availability on tablets, smartphones, and computers; its online and off-line accessibility; its worldwide diffusion-especially in the educational field; and the inclusion of automatic deduction and discovery tools, makes the use of these revolutionary ART techniques in GeoGebra a qualitatively different phenomenon with an unusually high potential for academic impact.

The purpose of this paper is, firstly, to make a summary presentation of the ART functions in GeoGebra through some illustrative examples of tasks showing how ART could be used within an educational context, helping students to develop “augmented intelligence” skills by reasoning in collaboration with the computer. Then we will reflect on the possible educational use of these new features, in particular through the analysis of some results of recent experiences we have developed with our students regarding the use of ART techniques.

Lastly, we will think about the advantages and disadvantages that this novelty could bring to the learning and teaching of geometry. As a final conclusion, we argue how that in order to fully benefit from this impressive tool, it will require that its use will become embedded in a larger ecosystem that should be developed by the scientific and teaching community, globally covering different aspects of computer-supported geometric reasoning Kovács et al. (2020).

2 GeoGebra Automated Reasoning Tools

This section introduces, describes, and exemplifies the technical features of some recently implemented Automated Reasoning Tools (ART) in the dynamic mathematics software GeoGebra. As mentioned above, these tools (given by a button in the Menu) and commands (to be introduced in the Command Line) allow the user to automatically conjecture, discover, and prove statements concerning different elements of a given geometric construction. Basic automated reasoning features are available since GeoGebra, version 5; yet, certain ART improvements and advanced characteristics can be found in GeoGebra Discovery, an experimental version of GeoGebra, available at https://github.com/kovzol/geogebra-discovery, operating on top of GeoGebra Classic 5, for computers and laptops, on Windows, Mac, or Linux operating systems; and the GeoGebra Classic, version 6, for browsers, accessible at http://autgeo.online/geogebra-discovery/, therefore valid also on tablets and smartphones.

Examples have been chosen that, on the one hand, illustrate the functionalities of ART tools in GeoGebra, and on the other hand, show the necessary interaction between human and machine reasoning, synthesizing into what we refer to here as “augmented intelligence” Semenov and Kondatriev (2020).

First of all, let us enumerate the list of GeoGebra’s Automated Reasoning commands:

• The Relation command and tool, for the automatic finding of properties that relate certain objects in a construction, that can be used, for instance, to check geometric conjectures and for the verification or denial of these conjectures. A complete list of the properties between geometric objects that Relation is able to obtain can be found at https://wiki.geogebra.org/en/Relation_Command.

• The LocusEquation command, which calculates the implicit equation of a certain semi-free point such that a given property holds.

• The Prove and ProveDetails commands, which decide if a statement is true in general and, eventually, give some additional conditions for its truth, avoiding degenerate cases.

• The Discover tool and command which finds a collection of statements holding true and involving a certain element selected by the user in the figure. This is a new feature, only available in GeoGebra Discovery.

Let us also mention that a detailed tutorial can be found in Kovács et al. (2018).

2.1 The Relation Tool and Command

This basic automated reasoning tool in GeoGebra is the symbolic extension of the previously existing Relation command. Initially, this command was purely numerical (see Kovács (2015a, b)): after the user has selected two geometric objects in a construction and invoked the Relation command (between the two objects), GeoGebra answered by asserting the possibility, or not, that certain relationships would occur between them, such as perpendicularity, collinearity, parallelism, equality, or incidence, as long as the numerical verification of such properties exceeded a certain threshold, with the user being warned in a message that the reached conclusion was only numerically valid.

In the current version of GeoGebra, the Relation command allows the user to click an additional button, labeled “More$\ldots$”, in the output message. By pressing this button, a symbolic calculation process is launched within the ART system of GeoGebra, translating the given geometric figure into a collection of polynomial equations and considering, systematically, as a thesis, the algebraic translation of the possible relations we have referred to, between the chosen geometric elements.

For instance, points can be considered as collinear for Relation, if by taking the line between two of them, the third one will turn out to be “approximately in the same line”, where “approximately” depends on the number of digits that the user has chosen in the application preferences (namely, in Tools $\triangleright$ Rounding in the user menu system of GeoGebra Classic 5, or in Settings $\triangleright$ Global $\triangleright$ Rounding in version 6) to perform calculations in the session with GeoGebra.

Example 1

Figure 1 shows a diagram with three collinear points A, B, and C, a free point O, and the midpoints D, E, and F of the segments OA, OB, and OC, respectively. In the Input Bar, the command Relation($\{D,E,F\}$) is introduced to study the existence, if any, of some property between the points D, E, and F.

The left part of Fig. 2 includes the response message to this command, which indicates that the points D, E, and F are, at least for this figure and approximately, collinear. Finally, Fig. 2, to the right, shows the result of pressing the icon “More$\ldots$”: it is the rigorous check of the general validity of the theorem that says that the midpoints of the different segments from a point to different points in a fixed line are collinear. It also warns the user that it is true except for a degenerate construction. Such verification is based on the execution of certain algorithms that involve, without the user perceiving it, several aspects of advanced computational algebraic geometry. See, for more technical details, Botana et al. (2015) or Recio and Vélez (1999).

Fig. 1

GeoGebra construction of the midpoints of the segments between a point O and three collinear points A, B, and C, and Relation($\{D,E,F\}$) inserted in the command line

Fig. 2

The numerical answer to the command Relation($\{D,E,F\}$) on the left and, to the right, the rigorous result after clicking on the icon “More$\ldots$”

The computational power of GeoGebra’s ART is not limited to basic geometric constructions, but is able to find and test much more sophisticated geometric relationships. For instance, we have considered a problem from one of the exams of the Spanish recruitment method to become a civil servant math teacher for the secondary school system. It is a method that requires passing and receiving the best grades on a series of public exams (also known as “oposiciones”). In one of these recent tests, the candidates were requested to solve the following elementary geometry question, which asked the test-writer, to conjecture, formulate and, then, to prove, the ratio holding between two particular segments in a given figure (see Fig. 3 from Gamboa et al. (2019)).

We used GeoGebra ART to perform this task in order to demonstrate how much it simplifies the solving of the problem, as well as how it involves a different way of reasoning through interaction with the computer.

Example 2

See the statement in Fig. 3, as given to the candidates. Then, the first challenge is to reproduce this picture as a GeoGebra construction.

To build the initial right triangle we have taken advantage of the fact that a right triangle, whose non-right angles are of $60^{\text {o}}$ and $30^{\text {o}}$, is half of an equilateral triangle (thus allowing us to start building a regular 3-sided polygon with the corresponding GeoGebra command Polygon). Then we have rotated vertices B and C $60^{\text {o}}$ counterclockwise twice, till $C''$ becomes aligned with A, B, as shown in Fig. 4.

Now we use the Relation tool to ask about any possible relation between segments $B'C$ and AN. Notice that this tool is usually utilized to find relations between exactly two objects in the construction; asking for any relation involving more objects, it is preferable to type Relation directly in the command line. It should also be noted that the computation of ratios between segment lengths through Relation is a new feature of this tool and command, currently only available in the prototype GeoGebra Discovery that we are here describing.

Fig. 3

Let ABC be a triangle with a right angle at B and with angles $60^{\text {o}}$ and $30^{\text {o}}$ at the other vertices. It has been rotated twice, both times centered at A and with equal rotation angle. Find the ratio $B'C/AN$

Fig. 4

GeoGebra construction of Fig. 3

Fig. 5

The numerical and symbolic  answers to Relation(r,q)

In Fig. 4 we show the position of the Relation tool in the toolbar. After clicking on the corresponding icon we select segments $B'C$ and AN, labeled as r and q respectively, and we obtain the numerical answer in a pop-up window, see the left of Fig. 5. After clicking on the “More$\ldots$” icon, a symbolic answer is displayed, as shown on the right of Fig. 5.

We leave to the reader the investigation of other surprising results concerning ratios of segments in this construction, for instance, the ratio between $BC'$ and AN.

2.2 The Prove and ProveDetails Commands

The Prove, ProveDetails commands work in a similar way. Unlike Relation, the user must enter the conjectured thesis (for instance, that the ratio between r and q is $\sqrt{7}/2$), obtaining as an answer the truth or falsity of their conjecture and, in the affirmative case, providing some additional geometric conditions that must be verified so that the given statement is generally true. These are the so-called non-degeneracy conditions, which usually prescribe that certain input objects (e.g., the free vertices of a triangle) must not coincide or be aligned, etc., for the conjectured statement to be true.

Fig. 6

After introducing ProveDetails(sqrt(7) q ==2 r) in the command line of GeoGebra, the obtained answer (in green) appears in the last line of the Algebra window

Figure 6 confirms the above-obtained relationship (Fig. 5) for Example 2. It means that the ratio $r/q=\sqrt{7}/2$ for the given construction holds true, except if points A and K (that were taken as free) coincide.

2.3 The LocusEquation Command

Another function that is made possible through the ART tools in GeoGebra is the discovery of new theorems, looking for complementary hypotheses for a certain thesis to hold. For instance, trying to generalize Example 2, we will now consider as initial hypotheses a similar construction, but starting with more general triangles, and we will try to find where to place vertex C in order to have same segment lengths ratio between AN and $B'C$.

Example 3

Let us start with a general (not necessarily equilateral) triangle ABC, and then let us roughly follow the previous construction, but with some modifications in order to end up with three, regularly rotated, triangles, ending up with A, B, and $C''$ aligned. Thus, instead of rotating vertex B and C, we are going to reflect vertex K with respect to the midpoint of AC and with respect to vertex A, yielding vertices $C'$ and $C''$, respectively (see Fig. 7). Notice that this construction ends up obtaining the same figure as the one in Example 2 that was built using rotations, and starting with an equilateral triangle.

Now, the command LocusEquation allows us to discover  for which triangles ABC the ratio $r/q=\sqrt{7}/2$ holds; more specifically, we ask GeoGebra, through the LocusEquation(sqrt(7) q ==2 r , C) command, where to put vertex C such that the required ratio holds.

In Fig. 8 the reader can see GeoGebra’s answer: to have the segment ratio $r/q=\sqrt{7}/2$, the vertex C must be placed in a cubic curve which is the union of a circle and a line (a degenerate case). Now it is the machine’s turn to challenge us to discover the geometric characteristics of this circle; GeoGebra cannot provide any further information about it. For instance, it seems that the center of the circle is in the reflection of point B with center K. But, what can we say about the radius?

Fig. 7

GeoGebra construction starting from a general triangle and taking midpoints and point reflections

Fig. 8

Typing LocusEquation(sqrt(7)q==2r,C) in the command line we obtain the equation of a curve in the Algebra window and its display (in purple) in the Graphics window

2.4 The Discover Tool and Command

The Discover  tool and command is a new feature currently available only in GeoGebra Discovery. This command searches, in an automatic and combinatorial way, for a whole series of possible geometrical relationships between the elements of the construction in which a point (pointed out by the user) is included, and then verifies its truth or falsity.

The use of this tool is illustrated with an old and challenging example that may be the object of an open-ended activity in which it will be necessary to explore, to discover, to conjecture, to prove, ...while applying some knowledge of elementary geometry, to reveal an enigma: the Treasure Island Problem.

Example 4

(Treasure Island Problem)

The Treasure Island Problem is described in Wilson (1997) where it is pointed out that “In 1948, George Gamow wrote a book called “One, Two, Three, ...Infinity”. In it, he presents a problem suggested by a treasure map found in a grandfather’s attic”. The problem is stated as follows:

A young man was going through the attic of his grandfather’s house and found a paper describing the location of a buried treasure on a particular island. The note said that on the island one would find a gallows, an oak tree, and a pine tree. To locate the treasure one would begin at the gallows, walk to the pine tree, turn right 90 degrees and walk the same number of paces away from the pine tree. A spike was to be driven at that point. Then return to the gallows, walk to the oak tree and turn left 90 degrees and walk the same number of paces away from the oak tree. Drive a second spike in the ground. The midpoint of a string drawn between the two spikes would locate the treasure.

The young man and his friends mounted an expedition to the island, found the oak tree and the pine tree but no gallows. It had been eliminated years ago without a trace. They returned home with the map above and no treasure.

Show them where to look for the treasure.

Why should we not help the young man and his friends to locate the treasure? Yes, we can try, assisted by GeoGebra ART!

We start by reproducing in GeoGebra the steps narrated in the paper to arrive to the treasure: we take three free points, representing the pine P, the oak O, and the gallows G, then we draw the segment from G to P and rotate it $90^{\text {o}}$ counterclockwise with center P to determine the point $S_1$. We do the same with the oak point O, but rotating clockwise to obtain the point $S_2$. Finally, we know that the treasure T is located at the midpoint of points $S_1$ and $S_2$ (see Fig. 9). As the story tells us that the gallows has disappeared, we can use GeoGebra’s dynamic capabilities to drag point G at random, trying to see the influence of this fading on the location of the treasure (compare the two maps in Fig. 9). Finally, one can become easily convinced, visually, that the position of the treasure does not depend on where we place point G.

Therefore, we conjecture that there must be some theorem linking the position of points P and O with that of T, but not involving a particular situation for G. Let us investigate the possible geometry theorems involving point T using the Discover tool: in the construction of Fig. 9 select the Discover icon in the toolbar and click the point T. GeoGebra computes a series of possible geometrical relationships between the elements of the construction in which point T is included. A pop-up window appears with the obtained theorems involving T (see Fig. 10).

Fig. 9

Using GeoGebra over the map of an island to get possible locations of the treasure for two different positions of the gallows

Fig. 10

Two GeoGebra windows after selecting the tool Discover and clicking at point T (equivalently, introducing Discover(T) in the command line). The pop-up window lists different geometric theorems involving T in different colors, and the Graphics Window displays, with the same colors, the geometric objects involved in these relationships

After discarding trivial relationships as well as those involving point G (that we assume is missing on the island), we have found the following conclusions:

• $OT=PT$, that is, the treasure (point T) is at the same distance from both trees (points P and O). The reader surely knows that this means that T lies within the perpendicular bisector of P and O; otherwise, GeoGebra ART can help us to discover where to put T such that $OT=PT$ by entering in the command line LocusEquation(Distance(P,T)==Distance(O,T)) (see Fig. 11, yellow line).

• $OT\perp PT$, that is the paths from the trees (P and O) to the treasure (T) are perpendicular. The reader surely knows also Thales’ Theorem and can deduce that T is in the circle passing through P and O having the segment PO as diameter; otherwise, GeoGebra ART can again help us to discover where to put T such that $OT\perp PT$ (see Fig. 11, purple circle).

A geometer “uncomfortable” with the result, could still require the student to prove that, starting from the initial configuration, point T verifies these two properties; this is achieved in Fig. 12.

Now, do not you consider that we could easily tell the young man in the story how to arrive at the treasure point, even not knowing where G was originally placed?

Fig. 11

Start drawing three points P, O and T and ask GeoGebra consecutively where to put T so that Distance(P,T)==Distance(O,T) and $OT\perp PT$. It yields T must be at the intersection of the yellow line and the purple circle

Fig. 12

Start with the construction in Fig. 10 and add the perpendicular bisector j of P and O, and the circle C centered at the midpoint of PO and passing by O. Ask GeoGebra to Prove($T\in j$) and Prove($T\in c$). The answer “true” for both commands appears in the Algebra window

3 Toward an Automated Geometer

In a certain sense, the ART tools we have described in the previous section can be considered as a kind of omniscient teacher, ready to answer whatever questions are posed by a human user—a sort of “geometry calculator.” Going a little bit further, a true “automated geometer” should be a kind of machine capable to investigating, without requiring any suggestion from humans, the geometric properties of a figure. Actually, this is already partially accomplished by GeoGebra Discovery, through the Discover command we have previously described, although it needs a human user to choose a concrete point in the given figure to focus the beginning of the discovery task. Thus, as a further step toward a completely independent performing “automated geometer,” we have implemented in GeoGebra  a new tool which we have called the Automated Geometer, that is a web-based service available at http://autgeo.online/ag, able to obtain, just by itself, sound relationships in a geometric construction.

Let us illustrate the behavior of the Automated Geometer by considering the ICMI Study series “School Mathematics in the 90s” Howson and Wilson (1986), dated back to 1986, which includes an elementary geometry question, as described in Fig. 13, item a), asking the user to decide if three given segments of the diagonal of a square are equal or not.

Fig. 13

A question from the so-called “Kuwait” ICMI Study, back in 1986

Let us roughly sketch how the question appearing in Fig. 13 can be solved by our Automated Geometer.

Fig. 14

The Automated Geometer on its startup

First, a web version of GeoGebra is loaded in the web browser and the user is asked to construct a geometric figure (or select one of the built-in examples). Five different options are then available to check certain properties holding in the figure: collinearity of three points, equality of distances between two points, perpendicularity of segments defined by two points, parallelism of segments defined by two points, and concyclicity of four points (see Fig. 14).

Once the user has decided among these options, and after having launched the discovery process, the Automated Geometer creates a list of possible statements in a combinatorial way (all possible triples of points are considered as potentially collinear, etc.) and calls the previously described automatic reasoning tools to verify or deny the truth of the considered propositions. For example, in the case of the Fig. 13, out of 1260 possible statements only 119 are true—all of these checks are performed within 9 s on a normal PC with 8$\times$i7 cores and 16 GB RAM, tested in Google Chrome 86. The obtained statements are visually presented in the program (see Fig. 15) and also a short list of them is printed (see Fig. 16). In particular, we mention that the proposed question is affirmatively answered considering items 21 and 22 in this Fig. 16.

Fig. 15

Visual results of automated discovery. The same colors usually refer to equality or parallelism

We highlight here that some unexpected results may also be included in the output. For example, concyclicity of points E, F, G, and H may be not completely trivial at the first look—one needs to find the axial symmetry through the diagonal BD to confirm this result. For other input figures, however, many more non-trivial facts can be eventually obtained. Actually, this is what we expect from discovery: we want to be surprised!

Fig. 16

List of obtained true statements of automated discovery

4 Discussion and Conclusions

It is clear that the above-considered Kuwait Study problem can be solved in various ways, traditionally by pure geometric means, but—as a more modern approach—the possibility of considering an algebraic solution is already mentioned in the 1986 ICMI Study Howson and Wilson (1986). The following sentences from this book are particularly relevant in our context:

...even more challenging, computer-based opportunities for transforming geometry teaching in the 1990’s will be provided by computer assisted design software which at the moment has had little impact on schools...As a result of recent curricular changes, the ‘few’, the mathematically gifted students, have at their disposal powerful algebraic tools, coordinates and vectors, which they can apply to geometric problems. They, then, might approach such problems in a different manner to school pupils of old—the methods may be less elegant, and provide less scope for creative and penetrating thought—but they offer a more systematic approach. ...whereas the student of the 1950s had only purely geometrical ways of tackling the problem [the authors refer to question (a) in Fig. 13], today’s student may well be able to apply algebraic methods ...The solution derived by applying a mechanical procedure may be less aesthetically satisfying than a geometrical one, but are there other objections to algebraic methods than that of aesthetics? (Howson and Wilson 1986, p. 58–59)

The quoted text reflects on the pros and cons of the different ways of solving the proposed question and states that an algebraic solution is maybe not as elegant as a geometric one, but “are there other objections to algebraic methods than that of aesthetics?”

As our methods rely heavily on the algebraic side, we sustain a very similar opinion, but in an even more radical form. In fact, the automated discovery process we have implemented in GeoGebra Discovery or in the Automated Geometer does not require any geometrical background in the proving process, since it starts translating mechanically every geometric relation into algebraic equations. Also, the obtained proof has nothing to do with geometry—it usually contains a large amount of variables and a number of polynomial equations of higher degrees, and then millions of elementary steps are required to obtain the required proof. Only the final translation of the algebraic results requires geometry again—a mechanical translation of the non-degeneracy results (some polynomials that should not be zero) back into geometric terms (e.g.,  some points should not be aligned).

In this approach, therefore, the whole proving, internal process is a kind of non-aesthetic operation and, what is more unaesthetic, in most cases, is the fact that it is completely unreadable for a human. On the other hand, this approach is extremely powerful for solving problems such as the one proposed in the ICMI Study, as it was already noticed by the ICMI Study authors concerning the use of “powerful algebraic tools” vs. the traditional, geometric technique. For example, anyone carrying a laptop, tablet, or smartphone, and using our GeoGebra automated reasoning and discovering tools, can quite easily solve, and even extend, some non-trivial problems, such as the one listed as number 230 in Chou’s collection of 512 mechanically proved theorems, included in his foundational monograph Chou (1998).

Fig. 17

Proving Chou’s problem 230

Indeed, nowadays it is quite straightforward to prove (with a commonplace laptop and without any appreciable time lapse) Chou’s original statement: “Show that the symmetric (symmetricA) of vertex A of a triangle (ABC) with respect to the midpoint (M) of the opposite side is collinear with the symmetric (symmetricO) of the orthocenter (Oorthocenter) with respect to A, and the circumcenter (circumcenter) of the triangle.” Thus Fig. 17 shows GeoGebra’s immediate proof of the statement $symmetricA \in linecircumcentersymmetricO$, where linecircumcentersymmetricO is the line defined by the circumcenter and the symmetric of the orthocenter, declaring it is true except when $A=B$ or A, B, C are collinear, that is, for degenerate cases.

Moreover, GeoGebra allows, as well, to conjecture of a generalized version of this theorem, analyzing if the same alignment thesis would hold for other choices of a center of symmetry D involved in building the point symmetricA. Thus, Fig. 18 shows, on top, in red, the locus of the possible positions of D for the collinearity of the three points symmetricA, symmetricO, circumcenter, namely, a parallel line to the one defined by the circumcenter and symmetricO, going through the midpoint M. In the same figure, below, it is verified that this collinearity holds true except for degenerate cases (the triangle ABC collapses to a line), when choosing as symmetry center any point D in the red line.

Fig. 18

Generalizing Chou’s example 230

It is evident for us, after all these examples that we have described so far, that teaching students having “...at their disposal powerful...tools which they can apply to geometric problems” Howson and Wilson (1986) cannot be a mere repetition of the traditional curriculum (in a broad sense: aims, goals, contents, methods, assessment, evaluation). Obviously, the training of the mind through the traditional approach to proving geometry theorems, has always been a crucial requirement for the development of mathematical skills.

Thus, we could consider addressing ICME-Study question a) in Fig. 13 without any auxiliary instrument, as a mere training task. But, while working on this question, can a student’s mind ignore that fact that in the school bag sitting next to her/him, there is a small machine that could answer the posed question in a moment? To put the question in a different context: are we equally motivated in climbing up mountains that have a cable car going to the top, when there are many others that cannot be so easily reached? Is it fun walking up stairs instead of taking the lift?

Thus, to overcome such drawbacks, we could ask ourselves: are there not other worlds of mathematical activities where we can exercise our reasoning techniques, and that are not already (or that can never be) automatized? Can we get profit of the “(obvious) assumption that computers exist” (Wolfram 2020, p. 4)?

We think that the answer to these questions is affirmative and that geometry and dynamic geometry systems with automated reasoning tools remain a very rich context for developing human reasoning skills. However, a context bringing a new, strong focus on open-ended tasks, as remarked in the Introduction: “...tasks where students are asked to explore objects and to discover and investigate their mathematical properties...” (Ulm 2011, p. 23). The idea is not new, but needs to be revisited: indeed, it was already back in 1995 that the father of automated reasoning in geometry, Prof. Wen-tsun Wu, stated that “...geometry problem solving instead of geometry theorem proving should be emphasized...” and that “algebra and geometry should be kept in pace in the teaching,” (Wu 1995, p. 72), without, apparently, much success in the “mainstream school maths curriculum.” (Wolfram 2020, p. 4)

Some examples regarding how to implement this new approach—i.e., merging open-ended tasks and problem solving in geometry and algebra with automated reasoning programs as fundamental tools—have already been implemented in some of our classrooms (reported in Recio et al. (2019)). A more recent contribution concerning the possible use of DGS reasoning tools in the classroom (i.e.,  proposing a workflow to incorporate these tools), aiming toward the development of an ecosystem for computer-supported geometric reasoning, appears in Kovács et al. (2020). Again, the repeatedly mentioned Kuwait Study provides another example of this new scenario that we would like to sketch out here as a final contribution. In fact, in the previous sections we have addressed just the first question in Fig. 13, noting that it can be easily solved using GeoGebra. Yet, question b) is of a different kind: it is an open-ended question in which the user is greatly benefited by having a DGS at hand for its exploration, but it is also a question that computers cannot automatically answer.

Obviously, if question a) deals with the division in two parts of the side AB of a square, its natural generalization should address the case of dividing the same side in n equal parts. Yet, GeoGebra reasoning tools cannot deal with a question that depends on n as a parameter...so all we can do is to experiment with different cases $n=3, 4, 5, \dots$ and try to find out if there is some common property holding in all these instances among the segments in the diagonal resulting from the intersection with the lines from the upper left vertex of the square to the points dividing the opposite side in $n=3, 4, 5, \dots$ parts. See Fig. 19 for the case $n=3$, where we have displayed only half of the lines, as the whole construction is symmetrical with respect to the DB diagonal and, thus, whatever properties that could be found on the segments AL, LM, MO in the figure could easily be stated for the full set of five segments.

Fig. 19

Kuwait ICMI Study question b) for $n=3$. By symmetry, only half of the construction is shown

One immediate way of generalizing question a) could be attempting to prove that all of the obtained segments are equal, but is easy to verify (e.g., using numerical approximation with GeoGebra’s Relation tool) that they are not. Another possibility is to consider if there is some algebraic combination holding among these segments, say, as it happens in the case $n=3$, that the sum of the first two and the last two is 4 times the middle segment (equivalently, that $AL+LM=4\cdot MO$, see Fig. 19), something that we can conjecture and quickly verify with the help of automated reasoning tools. But there are quite diverse possible algebraic expressions holding in the same construction (e.g.,  $AL=LM+MO$) and it is not easy to guess a general formula that takes place for all values of n.

Moreover, the geometric argument that we could have used (in a traditional approach to this question) for solving item a), i.e., that the barycenter of a triangle is twice more distant from the vertex than from the feet of the median, is obviously not applicable to the general case: we know nothing about properties of “tertians” (an invention of ours: lines from a vertex of a triangle to a point in the opposite side after dividing the side into three parts), etc. It could be a good opportunity to address this open-ended task, with the help of our digital tools, but question e) in the Kuwait problem requires us to now find a general formula, much beyond the case $n=3, \dots$ We do not want to spoil the solution to this intriguing question for the interested reader, but we can say that it has been very helpful for us to combine,

• DGS constructions, for visual conjecturing,

• Automated Reasoning Tools, for deciding the truth or falsity of our conjectures,

• Computer Algebra Systems (CAS) to handle formulas depending on parameters such as n, equal to the number of parts we divide side AB, or r, related to the point corresponding to the r/n-th part of the side.

A final reflection: we would argue that a wider, wiser, and deeper study of the potential curricular inclusion of these methodological changes is badly needed. Not only regarding GeoGebra Automated Reasoning capabilities, but also considering their connection to GeoGebra’s augmented reality tools (https://www.geogebra.org/m/RKYFdQJy) for exploring 3D-objects in the real world, as sketched in Botana et al. (2019).

In the meantime, the increasing, and already large number of GeoGebra users, over 100 million worldwide, is a decisive step toward making true this premonitory sentence from Hohenwarter et al. (2019): “as with pocket calculators, people will probably start using ART for checking geometric facts without the consensus of the pedagogical community on its role.”

Our education system cannot stay blind, for another 30 years—as those that have elapsed since the publication of the ICMI Study “School Mathematics in the 90s” Howson and Wilson (1986)—to the existence, advance, and availability of digital tools contributing to the development of mathematical activities.