Computer-Generated Geometry Proofs in a Learning Context

Abstract

Given its formal, logical, and spatial properties, geometry is well suited to teaching environments that include dynamic geometry systems (DGSs) , geometry automated theorem provers (GATPs), and repositories of geometric problems. These tools enable students to explore existing knowledge in addition to creating new constructions and testing new conjectures. In this chapter, we trace the evolution of current automatic proving technologies, how these technologies are beginning to be used by geometry practitioners in general to validate geometric conjectures and generate proofs with natural language and visual rendering, and foresee their evolution and applicability in an educational setting.

1 Introduction

Given its formal, logical, and spatial properties, geometry is well suited to teaching environments that include dynamic geometry systems (DGSs) , geometry automated theorem provers (GATPs), and repositories of geometric problems. These tools enable students to explore existing knowledge in addition to creating new constructions and testing new conjectures. With the help of a DGS, students can visualise geometric objects and link the formal, axiomatic nature of geometry (e.g., Euclidean geometry) with its standard models and corresponding illustrations (e.g., the Cartesian model) . With the help of GATPs, students can check the soundness of a construction (e.g., if two given lines are parallel) and also create formal proofs of geometric conjectures. Supported by repositories of geometric knowledge, these tools provide teachers and students with a framework and a large set of geometric constructions and conjectures for doing experiments.

In this chapter, we trace the evolution of current automatic proving technologies, how these technologies are beginning to be used by geometry practitioners in general to validate geometric conjectures and generate proofs with natural language and visual rendering, and foresee their evolution and applicability in an educational setting. Following Hanna’s (2000, p. 8) argument that “the best proof is one that also helps understand the meaning of the theorem being proved: to see not only that it is true, but also why it is true,” and the large number of articles on proof and proving in mathematics education from the ICMI Study 19 Conference (Lin, Hsieh, Hanna, & de Villiers, 2009a, 2009b), we focus our attention on practices of verification, explanation, and discovery in the teaching and learning of geometry.

In the classroom, the fundamental question a proof must address is “why?” In this context, then, it is only natural to view proofs first and foremost as explanations and, as a consequence, to give more value to those that provide a better explanation. Dynamic geometry systems encourage both exploration and proof because they make it so easy to pose and test conjectures. The feature that preserves manipulations allows students to explore “visual proofs” of geometric conjectures. Such a powerful feature gives them strong evidence that a theorem is true and reinforces the value of exploration by giving them confidence in a theorem.

The challenge facing classroom teachers is how to use the excitement and enjoyment of exploration to motivate students while also explaining that visual exploration is not a proof. Visual exploration is a useful aid, but is still only the exploration of a finite number of cases. One reason for giving students a formal proof is that exploration does not reflect the need for rigour in mathematics. Indeed, mathematicians aspire to a degree of certainty that can only be achieved by a proof. A second reason is that students should come to understand the first reason. As most mathematics educators would agree, students need to be taught that exploration, useful as it may be in formulating and testing conjectures, does not constitute a proof (Hanna, 2000; Hanna & Sidoli, 2007). A proof is a means of obtaining certainty about the validity of a conjecture (proof as a validation tool) and a strategy to further understand a formulated conjecture (proof as an instrument of understanding).

Geometry automated theorem provers open the possibility of formally validating properties of geometric constructions. For example: Cinderella¹ (Richter-Gebert & Kortenkamp, 1999) has a randomised theorem checker; Geometry Constructions LaTeX Converter (GCLC)² (Janičić, 2006) and GeoGebra³ (version 5) (Hohenwarter, 2002) incorporate a number of automated theorem provers that provide a formal answer to a given validation question (Botana et al., 2015; Janičić & Quaresma, 2007).

By means of the deductive database method (Ye, Chou, & Gao, 2010b), GATPs also enable students to explore new knowledge and discover new results and theorems (e.g., the algebraic formula of a loci (Abánades, Botana, Kovács, Recio, & Sólyom-Gecse, 2016; Recio & Vélez, 2012)). An important addition to any learning environment would be a GATP with the ability to produce human readable formal proofs with, eventually, visual counterparts (Chou, Gao, & Zhang, 1996a, 1996b; Janičić, Narboux, & Quaresma, 2012; Kovács, 2015; Stojanović, Pavlović, & Janičić, 2011; Stojanović, Narboux, Bezem, & Janičić, 2014).

In this chapter, we focus on the subjects of verification and explanation. Section 2 describes the past, present, and foreseeable future of geometry automated theorem proving. Section 3 uses examples to introduce the use of GATPs in the formal validation of a conjecture. In Sect. 4, we explore GATPs that produce readable formal proofs. In Sect. 5, we extend this exploration to GATPs that produce formal proofs with the addition of natural language and visual rendering. In Sect. 6, we draw conclusions and anticipate future avenues of research.

2 Formal Geometric Proofs

Given the cognitive complexity of geometric activities, learning geometry is not always immediate or easy. However, visualisation can be used to understand proofs and help mathematical reasoning. Visual elements attract students’ attention, raise their awareness, and help them make connections between subjects and concepts. Visualization contributes to a better understanding of the results obtained from a search for different approaches to solving a problem or proving a theorem. It promotes new forms of reasoning that can inspire simple and elegant solutions to similar problems, allowing students to respond to more complex problems or prove new theorems (de Villiers, 2006).

Introducing DGSs in the learning process enables greater experimentation than previous tools did. DGSs allow free geometric objects to be continuously modified, thereby keeping geometric properties unchanged. Although these manipulations are not formal proofs because only a finite set of positions is considered and because visualisation can be misleading (when the image, for example, refers to a particular case), they provide a first clue to the truthfulness of a given geometric conjecture (Hoyles & Jones, 1998; Nelsen, 1993; de Villiers, 2006). It can be said that DGSs provide an initial non-formal link between theories and models of geometry (Janičić & Quaresma, 2007; Ruthven, Hennessy, & Deaney, 2008).

Geometry automated theorem provers similarly enhance learning. First, they can be used to validate a geometric construction such as: are two given lines parallel? The answer—yes!/no!/cannot be established—is a “black box” approach (it does not answer the “why”), but can be useful in situations where formal proofs are not being considered. Second, some GATPs are able to provide formal proofs—not only the answer to a question, but also the “why.” As said above, this constitutes the “best proof.”

Unlike DGSs that are similar in their approach and capabilities, GATPs vary significantly in terms of the method they use (e.g., synthetic vs. algebraic), the implementation (e.g., area vs. full-angle), and the output (formal proof vs. only a yes/no answer) (Chou & Gao, 2001; Chou, Gao, & Zhang, 1994; Quaresma, 2017; Wang & Su, 2015; Wu, 1984). According to Jiang and Zhang (2012), consideration needs to be given to the somehow opposite goals of efficiency and readability. Efficiency is important because, in a learning situation, it is not viable to wait more then a couple of seconds to get an answer. Readability is important given that, without it, the “why” would be lost.

The first methods proposed in the 1950s adapted general reasoning approaches from the field of artificial intelligence to the automation of traditional geometric proving processes. In order to avoid combinatorial explosion while applying postulates, many suitable heuristics were used; for example, adding auxiliary elements to geometric configurations, and using the corresponding geometric constructions as a source of counterexamples to help the reasoning procedure choose the right path. Although these methods produced readable proofs that could be used in learning, they were very narrow in scope and inefficient (Wu, 1984). However, some recent results using this approach in education focus on developing GATPs scoped for a given set of problems (Paneque, Cobo, Fortuny, & Richard, 2016; Richard, Oller Marcén, & Meavilla Seguí, 2016). Still, its usefulness in education has yet to be established.

The next step in creating more generic, powerful, and efficient provers was to integrate algebraic methods such as the characteristic set method (also known as Wu’s method) (Chou, 1985; Wu, 1984), the polynomial elimination method (Wang, 1995), the Gröbner based method (Kapur, 1986), and the Clifford algebra approach (Li, 2000). These methods reduced the complexity of logical inferences by computing relations between coordinates of geometric entities. The corresponding implementations could successfully solve many complicated geometric problems and discover new theorems. However, human readability of the proofs was lost, and the algebraic proofs were complex and not related to geometric reasoning (Chou et al., 1994; Wu, 1984). Nonetheless, there are many recent implementations of these methods (Botana et al., 2015; Janičić et al., 2012; Janičić & Quaresma, 2006; Kovács, 2015; Ye, Chou, & Gao, 2011) and, in Sect. 3, we explore the possible use of these GATPs in education.

In an effort to combine the readability of synthetic methods and the efficiency of algebraic methods, some approaches, such as the area method (Chou et al., 1996a; Janičić et al., 2012) and the full-angle method (Chou et al., 1996b), represent geometric knowledge with respect to geometric invariants. These methods and some of their implementations are capable of proving a large number of complex geometric theorems and, in many cases, rendering the proofs in readable natural language. In Sects. 4 and 5, we describe this innovation in length.

3 Verification of the Truth of a Geometric Statement

Dynamic geometry programs give users an initial visual validation of a geometric property. Instead of producing a fixed example, these programs produce a large set of examples that reinforce confidence in the truth of a statement. However, given that not all possible cases can be covered, this can be misleading.

GeoGebra has had, since an early version, a validation tool, the “$a\,{\mathop {=}\limits ^{?}}\,b$” tool. This tool performs a numerical verification instead of a formal proof, and suffers from the fact that numerical errors may led to erroneous conclusions. However, since version 5, GeoGebra has been enhanced with the support of GATPs. This makes it possible to ask for a formal validation of a given geometric statement (Botana et al., 2015) such as the Midpoint Theorem.

Theorem 1

(Midpoint Theorem) Let ABC be a triangle, and let D and E be the midpoints of $\overline{AB}$ and $\overline{BC}$ respectively. Then the line DE is parallel to the base AC.

Having made the geometric construction (see Fig. 1), a GeoGebra user can check if the conjecture is indeed true. Entering the command “Prove (AreParallel(b,f))” produces the answer “d=true” (see Fig. 1). This is a formal validation generated by GeoGebra’s built-in GATPs.

Fig. 1

GeoGebra construction validation

Other DGSs also have integrated GATPs. For example, GCLC incorporates GCLCprover, which gives the following response to a similar situation (Janičić & Quaresma, 2007):

Deduction check invoked: the property that led to the error will be tested for validity.

Once the conjecture is successfully proved, the critical property always holds. The prover output is written in the file error-proof.tex.

A similar approach is used by the DGS/GATP Java Geometry Expert (JGEX)⁴ (Ye et al., 2011). It calculates fix-points during the construction; that is, all the properties that can be inferred from the construction to a certain point. When a user tries to perform an illegal construction, the tool says why it is not possible to perform that construction (see Fig. 2).

Fig. 2

JGEX construction validation, $\overline{FE}\ ||\ \overline{AB}$

If we jump to “explanation”—providing insight into why a given statement is true—we need to consider proofs. In the next two sections, we explore the capabilities of current GATPs to produce readable proofs with a natural language and even visual rendering.

4 Proofs with a Natural Language Rendering

Some of the methods used for geometric automated theorem proving, especially algebraic methods, are not useful in terms of the proofs produced. After a synthetic geometric representation is converted to an algebraic representation, the proofs are all done using complex algebraic reasoning without any connection to the geometric construction. The algorithms implemented in GeoGebra are of this type. They produce a time efficient answer to a verification problem, but are useless if the proof itself is the focus.

In (2010a), Ye et al. list the features they feel important to the dynamic visualisation of proofs in geometry. The first of these features is that “The proof text created by the program should be readable, similar to proofs in geometry textbooks or books.”

The semi-synthetic methods like the area method, the full-angle method or the deductive database method, along with the coherent logic based method, are able to produce readable geometric proofs. Implementations like the GCLC (area method) (Janičić et al., 2012; Quaresma, Janičić, Tomašević, Vujošević-Janičić, & Tošić, 2008), the JGEX (area method, full-angle method, and deductive databases)(Ye et al., 2010a, 2010b, 2011) and the ArgoCLP⁵ (coherent logic)  (Stojanović et al., 2011) are examples of systems with such capabilities.

The Area Method The area method is a decision procedure for a fragment of Euclidean plane geometry. It deals with problems as sequences of specific geometric construction steps, using a set of specific geometric quantities to define relations (Janičić et al., 2012).

• Ratio of parallel directed segments, denoted $\overline{AB}/\overline{CD}$. If the points A, B, C, and D are collinear, $\overline{AB}/\overline{CD}$ is the ratio between the lengths of directed segments AB and CD. If the points A, B, C, and D are not collinear, and it holds $AB \Vert CD$, there is a parallelogram ABPQ such that P, Q, C, and D are collinear and then $\frac{\overline{AB}}{\overline{CD}}=\frac{\overline{QP}}{\overline{CD}}\;.$

• Signed area for a triangle ABC, denoted $\mathcal {S}_{ABC}$ is the area of the triangle ABC, negated if ABC has a negative orientation.

• Pythagoras difference,⁶ denoted $\mathcal {P}_{ABC}$, for the points A, B, C, defined as $\mathcal {P}_{ABC}=\overline{AB}^2+\overline{CB}^2-\overline{AC}^2$.

These three geometric quantities allow for expressing (in the form of equalities) geometry properties such as the collinearity of three points, the parallelism of two lines, the equality of two points, the perpendicularity of two lines, and so forth (see Table 1).

Table 1 Expressing geometry predicates in terms of area method geometric quantities

The basic objects in an area method conjecture are the points—free points if they are freely placed in the Euclidean plane, and constructed points if they are obtained as the result of a given geometric construction. For example, in the Midpoint Theorem (see Theorem 1) the points A, B and C are free points not defined by construction steps. The constructed points D and E are the midpoints of $\overline{AB}$ and $\overline{BC}$ respectively.

The proof of a conjecture is based on eliminating all the constructed points in reverse order until equality is reached in only the free points. If the equality is provable, then the original conjecture is also a theorem. For Theorem 1, the proof automatically found by GCLCprover (see Fig. 3) shows not only the steps leading to the solution, but also the justification for those steps. GCLCprover uses the axioms and rules of inference of the area method to reach the conclusion in 16 steps, of which only 5 are applications of lemmas of the method (e.g., Lemma 29).

Fig. 3

GCLCprover output—Proof of Midpoint Theorem

The area method implementation in GCLC took 0.001 s to prove the Midpoint Theorem. It also found that there are no non-degenerated conditions to this result; that is, it is true in any configuration.

Given that the area method does not follow the normal chain of geometric reasoning used in primary and secondary schools, the resulting proofs are not directly usable by students. However, with the help of teachers, the area method (the full-angle method is similar) could be used at secondary and college levels. This claim needs validation by case studies (see Sect. 6).

The Full-Angle Method The full-angle method is similar to the area method, but introduces the full-angle as another geometric quantity. Intuitively, a full-angle, $\angle [u, v]$, is the angle from line u to line v (not between segments).

Formally, full-angles can also be defined using the signed area and the Pythagoras difference. A full-angle is defined as an ordered pair of lines which satisfies a set of axioms and rules of inference that constitute the base of the method. The proofs are similar to those using the area method (Chou et al., 1996a).

The JGEX system implements the full-angle method and the deductive database method (based on full-angle rules). Using the full-angle prover, the Midpoint Theorem (see Theorem 1) can be proved (see Fig. 4) in a very concise form. However, the JGEX system does not produce a PDF output file.

Fig. 4

JGEX screen capture—Proof of Midpoint Theorem

Like the area method proofs, the use of full-angle method proofs in primary and secondary levels is limited by the axioms and rules of inference used. JGEX does not produce a proof with a natural language rendering. Unless the reader is familiar with the axiom system and corresponding inference rules, the proofs are somehow difficult to follow.

Coherent Logic Provers  A different approach is given by the ArgoCLP, a coherent logic-based theorem prover. Coherent logic is a fragment of first-order logic where the conjectures can be proved directly (i.e., not by refutation) . Proofs in coherent logic are natural and intuitive, and reasoning is constructive (Bezem & Coquand, 2005). Coherent logic is therefore a suitable framework for producing both readable and formal proofs. The ArgoCLP automatically and simultaneously generates traditional human readable proofs and formal proofs of geometry theorems (for various axiom systems). The generated step-by-step proofs are very similar to the proofs given in standard geometry textbooks. Unfortunately, however, efficiency issues prevent its use in education (Stojanović et al., 2011, pp. 13–14).

5 Proofs with Natural Language and Visual Rendering

Given the current implementations in geometry automated theorem proving, it is now possible to begin work on a new approach: proofs that interrelate geometric elements in the proof text and the construction.

As Ye et al. (2010a) show in their features of visually dynamic proofs in geometry, effective connection between the visual rendering and textual rendering is key:

The displays of the proof text and the geometry elements in the construction are separated, but should be internally related. By clicking a step or a part of a step of the proof’s text, the corresponding geometric elements in the construction should be highlighted using various dynamic visual effects.

They propose visual effects such as translations, rotations, reflections, and scaling to show congruence and similarities between geometric elements. Colours and blinking effects can be used to show the relations between the two renderings of a proof.

As discussed above (see Sect. 4), natural language rendering is possible and usable with some limitations in different contexts. Is it possible to connect natural language rendering with a formal proof and visual rendering? In the following, we examine the strengths and challenges of different approaches.

Fig. 5

Illustration for area method geometric quantities

5.1 Area Method Visual Rendering of Proofs

As mentioned above (see Sect. 4), the area method deals with problems stated as sequences of specific geometric construction steps, using a set of specific geometric quantities (Chou et al., 1996a, 1996b; Janičić et al., 2012). In the following, we establish a connection between the axioms and inference rules of this method. Using this connection makes it possible to synchronize a formal proof, a natural language rendering, and a visual rendering.

Visual Counterparts of Geometric Quantities The ratio of parallel directed segments and the signed area have a clear visual counterpart. The Pythagoras difference needs the support of the algebraic quantity $\overline{AB}^2+\overline{CB}^2-\overline{AC}^2$ (see Fig. 5).

Axioms and Lemmas of the Area Method The area method uses a large set of lemmas that characterise the geometric quantities and facilitate structuring the proofs (Chou et al., 1996a; Janičić et al., 2012; Quaresma & Janičić, 2009). Many of these lemmas are about technical issues related to the formal proofs; for example, how two triangles that differ only in the order of their vertices can be considered the same. The most important for area method proofs and also for their visualisation are the elimination lemmas.

In the following, we introduce two of these lemmas and present their visual counterparts.

Theorem 5.1

(Elimination Lemma 1—The Co-side Theorem) Let M be the intersection of two non-parallel lines AB and PQ and $Q \ne M$. Then it holds that $\frac{\overline{PM}}{\overline{QM}} = \frac{\mathcal {S}_{PAB}}{\mathcal {S}_{QAB}};$ $\frac{\overline{PM}}{\overline{PQ}} = \frac{\mathcal {S}_{PAB}}{\mathcal {S}_{PAQB}};$ $\frac{\overline{QM}}{\overline{PQ}} = \frac{\mathcal {S}_{QAB}}{\mathcal {S}_{PAQB}}$ (Fig. 6).

Fig. 6

Illustration for elimination Lemma 1: $\frac{\overline{PM}}{\overline{QM}} = \frac{\mathcal {S}_{PAB}}{\mathcal {S}_{QAB}}$

Theorem 5.2

(Elimination Lemma 3 (reduced version)) Let $\mathcal {S}_{ABY}$ be the $\Delta ABY$ signed area where point Y is the intersection of lines UV and PQ. Then it holds that (Fig. 7)

$$ \mathcal {S}_{ABY}=\frac{\mathcal {S}_{UPQ}\mathcal {S}_{ABV}-\mathcal {S}_{VPQ}\mathcal {S}_{ABU}}{\mathcal {S}_{UPVQ}}. $$

Fig. 7

Illustration for elimination Lemma 3: $\mathcal {S}_{ABY}=\frac{\mathcal {S}_{UPQ}\mathcal {S}_{ABV}-\mathcal {S}_{VPQ}\mathcal {S}_{ABU}}{\mathcal {S}_{UPVQ}}$

Area Method Visual Proof—Midpoint Theorem Using the visual counterparts of the lemmas of the area method we can revisit the Midpoint Theorem (see Theorem 1). This time the GCLCprover area method proof has two parts: a natural language part and a visual counterpart.

The example illustrates how to express a problem using the given geometric quantities and how to prove it in a concise, easily understood way with a corresponding visual rendering.

As far as we know, there are no systems for the area method that provide such a connection. It is not yet a feature of GCLC (see Sect. 6). However, JGEX (Ye et al., 2010a, 2010b, 2011) does provide this connection for the full-angle method.

5.2 Full-Angle Method Visual Proofs

Using the JGEX system, we can build a given construction, state a conjecture about it, and then, using one of the built-in GATPs, prove it. Using the full-angle method based GATP we can produce examples where the formal proof has a visual counterpart.

Figure 8 was taken from the tool’s own set of examples. Clicking on a step of the formal proof produces a visual animation of the step on the construction. The related relations between objects on the construction—e.g. the angles between two lines in Fig. 8 (left)—initially “blink.” They then become fixed, but use colours to clearly show the corresponding relations in the formal proof.

Fig. 8

JGEX—Example 84, Steps 2 and 5

In both situations, the drawback is that neither the area method nor the full-angle method use the usual set of axioms and rules of inference of primary and secondary school geometry. Instead, they use the geometric quantities ratio of parallel directed segments, signed area, Pythagoras difference and full-angle, and the axioms and rules of inference for these geometric quantities. Using these methods in secondary schooling could prove difficult.

6 Conclusions and Future Work

Geometry, with its very strong and appealing visual content and its formal axiomatic theory, is a privileged domain. It is an area where computational tools can significantly enhance the learning environment and make students active in building their knowledge.

Introducing dynamic geometry systems enhances exploration and proof by making it easy to posit and test conjectures. The ability to make, properties-preserving, manipulations enables students to explore “visual proofs” of geometric conjectures. DGSs significantly help students to acquire knowledge about geometric objects and, more generally, to acquire mathematical rigour.

Geometry automated theorem provers capable of construction validation and human readable proofs consolidate the knowledge acquired with the use of DGSs. If the GATP produces synthetic proofs, the proof of a conjecture or the proof of the soundness of a construction can be used as an object of study providing a logical explanation. With a DGS, students can visually explore constructions or check that certain conjectures are true. However, these systems do not provide mathematical arguments for the conclusions they produce. Instead of producing a “visual check,” a GATP can be used to draw accurate mathematical conclusions. Thus, we claim that GATPs can be used in the learning process (Janičić & Quaresma, 2007; Quaresma & Janičić, 2006; Santos & Quaresma, 2012, 2013).

The natural language rendering of a formal proof, especially if paired with a visual rendering, would allow for a wider application of GATPs in learning contexts. This is still an active area of research involving exploration of different methods, implementations, and renderings. Currently, we are exploring the construction of a controlled hybrid language for geometry; that is, a pair of controlled languages (natural and visual) with common semantics. By considering figures as sentences in a visual language sharing semantics with the natural language of geometric statements, we can achieve interaction between parts of text and corresponding figures. We can connect formal proofs to natural language and visual descriptions. This approach is more generic than the concrete cases described above. It is a line of research we are already pursuing.⁷

Given the availability of GATP technology and the work currently being done on the rendering of the proofs, it is important to begin integrating these advances in learning environments. As authors, we have already developed the Web Geometry Laboratory (WGL),⁸—an adaptive and collaborative blended-learning Web environment that integrates a dynamic geometry system (Quaresma, Santos, & Bouallegue, 2013; Quaresma, Santos, & Marić, 2018; Santos, Quaresma, Marić, & Campos, 2018). A short/medium term goal of the WGL is to connect with the OpenGeoProver (OGP)⁹ (Baeta & Quaresma, 2013), an open library of GATPs that we are currently developing alongside with others researchers. The connection between WGL and OGP will provide the lab with the automatic deduction capabilities discussed in this chapter; namely, checking the validation of a construction and getting formal proofs with a human readable and visual rendering (Quaresma & Santos, 2016). This and other projects like the integration of GATPs in GeoGebra (Botana et al., 2015) aim to include the power of automatic deduction in the learning and teaching of geometry. Ultimately, our goal is to help teachers and students answer the question “why.”