Keywords

1 Introduction

Logic appears in a sacred and in a profane form. The sacred form is dominant in proof theory, the profane form in model theory

D. van Dalen, Logic and Structure (van Dalen, 1980)

Sacred Form

It can be said that the sacred form began circa 300 BC with the writing of Euclid’s Elements. The Elements can be seen as a seminal work, establishing the basis for proof theory, with a collection of definitions, postulates, propositions (theorems and constructions) and mathematical proofs of the propositions. For centuries, it was included in the curriculum of the majority of the universities. For example, in 1692 Tirso de Molina, Superior General of the Jesuit Order wrote a letter with very specific orders to improve the teaching of Mathematics at the Portuguese province (i.e. Universities of Coimbra and Évora). One of the suggestions was the reproduction of the figures in the Elements in such a way that all the students could see those figures and discuss about the geometric properties behind those figures. The combination of that letter with the Portuguese tradition of tilling (“azulejos”) gave rise to a collection of tiles with faithful representation of many of the figures in the Elementa Geometriæ by the Jesuit priest André Tacquet (1612–1660) (see Fig. 1) (Gabriel Silva, 2017; Simões, 2007).Footnote 1

Fig. 1
figure 1

Azulejos with figures from Elementa Geometriæ by André Tacquet

Full size image

David Hilbert in his book Grundlagen der Geometrie (1899) established the foundation for a modern axiomatic treatment of Euclidean geometry (Hilbert, 1977). Later, Alfred Tarski built a decision method for elementary algebra and geometry (Tarski, 1951) allowing constructive and even automated approaches for geometry (Beeson, 2015; Quaife, 1989) and, more recently, (1995) Jan von Plato proposed another constructive approach to geometry (von Plato, 1995).

From a computational perspective, the history of geometry automated theorem provers (GATP) began with the early computers and the birth of Artificial Intelligence, in the 1960s. The different sets of axioms of Euclidean Geometry attracted researchers to an attempt to implement synthetic methods, such as the approaches by Gelernter (1995, 1960), Nevis (1975), Elcock, Greeno et al. (1977), Coelho and Pereira (1979, 1986), Chou et al. (1993, 1995). The difficulties found with the synthetic methods, where the need to find a suitable rule to be applied lead to a combinatorial explosion regarding all the possible choices. This resulted in the exploration of other approaches, algebraic, semi-synthetic and logical approaches.

The algebraic style approach is characterized by the translation of geometric problems to algebraic problems, and subsequent development of the proof by the application of algebraic manipulations. The characteristic set method, also known as Wu’s method (Chou, 1985; Wu, 1984), the elimination method (Wang, 1995), the Gröbner bases method (Kapur, 1986a, b) and the Clifford algebra approach (Li, 2000) are examples of practical methods of this type. The algebraic approach led to efficient implementations, but, given that all the proofs are developed by algebraic means, the geometric meaning is lost, i.e. apart from a yes/no answer, it is not possible to have a correspondent geometric proof where the axioms of geometry are used. This led to the development of methods capable of, at least partially, combine the geometric readability of synthetics methods with the efficiency of algebraic methods.

The semi-synthetic methods use a set of specific geometric quantities, e.g. the ratio of parallel directed segments and signed area, to build an axiom system where the geometric relations and properties can be represented and the proofs developed using a set of geometric lemmas and simple algebraic manipulations. Examples of such methods are the area method (Chou et al., 1996a; Janičić et al., 2012) and the full-angle method (Chou et al., 1996b). These methods combine the readability of synthetic methods and the efficiency of algebraic methods, being able to prove many geometric theorems, efficiently and with geometric, readable, proofs.

More recently (2000–till present), new synthetic approaches are being proposed; the geometric deductive database method combines the full-angle axiom system with the techniques of deductive databases to develop an efficient GATP capable to prove a large set of geometric problems (Chou et al., 2000). Also tutorial systems like the QED-Tutrix (Gagnon et al., 2017; Tessier-Baillargeon et al., 2017) are proposed to address the problem in a more contained form, i.e. instead of trying to implement a generic GATP, the goal is to have an efficient and capable of readable geometric proofs GATP, to specific areas of geometry.

Also to be considered are the logical approaches, like the quantifier elimination method of Tarski (Collins, 1975; Tarski, 1951), or the use of axiom systems for geometry (e.g. Tarski, Quaife (1989)) and then using generic automated theorem provers (ATP) to develop the proofs. Many efficient and capable of proving many geometric conjectures ATP are available, but, like in the algebraic approach, the proof has no correspondence with any form of geometric reasoning. From the view point of a geometer, it is difficult to follow (geometrically) the formal proofs produced by the ATP.

Profane Form

The Profane form came with programs that allow to build and explore geometric figures. The 1988 Turing prize was awarded to Ivan Sutherland for his pioneering work in the area of computer graphics. The program Sketchpad changed the way people interacted with computers, from non-graphical to graphical (Sutherland, 1963, 2003). While the original aim was to make computers more accessible, introducing graphical manipulations, while retaining the powers of abstraction that are critical to programmers, the direct manipulation interfaces have since succeeded by reducing the levels of abstraction exposed to the user.

The program Sketchpad can be considered as the point of origin for today’s computer-aided graphic design programs (CAD). Not detracting from CAD programs, they are of little interest for the geometry practitioner, they are very high-precision tools to draw figures, e.g. for architects, drawing building plans, but they miss the step from drawings (static object) to figures (geometric construction), i.e. a set of objects and geometric relations between then (dynamic object). Meanwhile, dynamic geometry systems (DGS) allow building geometric constructions from free objects and elementary constructions. It became possible to manipulate the free objects (objects universally quantified), preserving the geometric properties of the construction.

The first software packages that can be classified as dynamic geometry systems were Geometer’s Sketchpad (Jackiw, 2001), which appeared first in 1989, and Cabri Géomètre (Laborde & Strässer, 1990), dating back to 1988, and they started another revolution: computers could be used in school for teaching geometry. Since then DGS become mature tools used by millions of users all over the world.

Fig. 2
figure 2

Gelernter—Angle bisection

Full size image

Dynamic geometry systems gave us the profane side of proofs in geometry. For example Fig. 2 (if done with a modern DGS) would have the points A, B and C as free points and point D as a constructed point (intersection of lines), moving the free points we can conjecture that the segments AD and CD are equal in length, i.e. we are exploring “all” possible configurations for a given geometric construction in the Cartesian model. Although those manipulations are not formal proofs because only a finite set of positions are considered and visualization can be misleading, they provide a first clue to the truthfulness of a given geometric conjecture.

The DGS and GATP are in a collision course and that is a good thing. From the development of GATP and DGS as completely separated tools, to the implementation of some GATP method in a DGS (e.g. Cinderella) or graphical components into a GATP (e.g. GCLC and JGEX) to the integration of GATP and DGS (e.g. GeoGebra). The fully integration of automated deduction components in other software is becoming a reality and it is expected that in a near future it will be possible to have those components broadly available.

Overview of the chapter In Sect. 2, the evolution of automated deduction in geometry is presented and in Sect. 3 the integration of  GATP and DGS is discussed. In Sect. 4 other lines of research are presented and in Sect. 5 conclusions are drawn.

2 Automated Deduction in Geometry

For the last five decades, automated deduction in geometry, the sacred form, has been an important field in the area of automated reasoning. Various methods and techniques have been studied and developed for automatically proving and discovering geometric theorems (Chou, 1987; Chou & Gao, 2001; Chou et al., 1994).

2.1 Synthetic Methods

Adapting general-purpose reasoning approaches developed in the field of artificial intelligence (in the 60s of the twentieth century), synthetic methods, such as the approaches by Gelernter (1995, 1960, Nevis (1975), Elcock (1977), Greeno et al. (1979), Coelho and Pereira (1979, 1986), Zhang et al. (1995), were dedicated to automating traditional proving processes (Chou & Gao, 2001). Making use of axiomatic systems close to the ones used in secondary schools these systems tried to provide readable (by students and teachers) proofs. See Fig. 2 for an example of such proofs, from the GATP by Gelernter.

In many of these first attempts, the diagrams where used as a model (Coelho & Pereira, 1986):

  • the diagram as a filter (acting as a counter-example);

  • the diagram as a guide (acting as an example, suggesting eventual conclusions).

As a filter the diagram permits to test the non-provability of a candidate sub-goal, pruning the proof tree.

Fig. 3
figure 3

Coelho et al. (1986)—Diagram as a guide

Full size image

As a guide the diagram can be used as a positive indication. Quoting from Coelho et al. (1986) Coelho and Pereira (1986) (see Fig. 3):

We want to prove two equal segments \(UV = XY\), by congruent triangles. Suppose triangle XYZ exists, and our purpose is to find a triangle UVW on UV to compare to triangle XYZ. We need to search for existing or generated triangles on UV. The first thing is to find a convenient third point W, which must be different from U and V. The possible coordinates of the sought point W are computed from the coordinates of X, Y, Z, U and V, and a check is made in the diagram to see if a point with such coordinates exists. The diagram is used in a positive way for computing the possible coordinates for W.

The possibility of having geometric proofs, with natural language and (eventually) visual renderings, is a key aspect of this approach. Unfortunately, the combinatorial explosion while applying postulates implied the use of suitable heuristics that narrow the scope of the GATP and prevent the development of a general-purpose efficient GATP.

New synthetic approaches are being proposed. The geometric deductive database method combines the full-angle axiom system with the techniques of deductive databases, to develop an efficient GATP capable of proving a large set of geometric problems (Chou et al., 2000). A coherent logicFootnote 2 based GATP, ArgoCLP, is being developed which can be used to generate both readable and formal (machine verifiable) proofs in various theories, primarily geometry. The possibility of, using a top-down approach (from the conjecture to the conclusion), producing natural language proofs is a positive point, but, efficiency considerations are still a major concern (Stojanović et al., 2011).

2.2 Algebraic Methods

A different approach is given by the algebraic style methods, given by the translation of geometric problems to algebraic problems and the subsequent development of the proof by the application of algebraic manipulations. The characteristic set method, also known as Wu’s method (Chou, 1985; Wu, 1984), the elimination method (Wang, 1995), the Gröbner bases method (Kapur, 1986a, b) and the Clifford algebra approach (Li, 2000) are examples of practical methods based on the algebraic approach.

Let us consider, for example, the Euler’s Line theorem.

Theorem 1

(Euler’s Line Theorem) In any given triangle, the orthocentre, the centroid and the centre of the circumscribed circle are collinear (Fig. 4).

Fig. 4
figure 4

Euler’s line theorem, JGEX construction

Full size image

Transcribing it to algebraic form we get (GATP: JGEX, Wu’s method):

figure a

At this stage the geometric/algebraic connection is still possible, each geometric element has a correspondent set of algebraic equations and vice versa. In the proof itself, pure algebraic methods are used. In Wu’s method, this implies calculating triangular systems and pseudo-remainders (Chou, 1985; Wu, 1984).

The JGEX’s proof (Wu’s method) is:

figure b

GATP based on these methods are efficient and able to proof a large number of geometric conjectures. The price to pay is the absence of geometric proofs and the algebraic proofs, if any, are only (barely) readable by experts (Chou & Gao, 2001).

2.3 Semi-Synthetic Methods

In order 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 in the form of expressions with respect to geometric invariants.

For stating and proving conjectures, these methods use a set of specific geometric quantities that enable treating geometric relations defining an axiom system. Considering the area method, we have:Footnote 3

  • 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, multiplied by \({-}1\), if ABC has the negative orientation.

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

An axiom system based on these three geometric quantities allows expressing (in form of equalities) geometry properties such as collinearity of three points (\(\mathcal {S}_{ABC}=0\)), parallelism of two lines (\(\mathcal {S}_{ABC} = \mathcal {S}_{BCD}\)), equality of two points (\(\mathcal {P}_{ABA}=0\)), perpendicularity of two lines (\(\mathcal {P}_{ACD}=\mathcal {P}_{BCD}\)), etc. (Chou et al., 1996a; Janičić et al., 2012).

Fig. 5
figure 5

Euler’s line theorem, GCLC proof (area method)

Full size image

To prove a given conjecture, we have to express the hypotheses of a theorem using a set of starting (“free”) points and a set of constructive statements, each of them introducing a new point, and to express the conclusion by an equality between polynomials in the geometric quantities of the method (without considering Cartesian coordinates). The proof is developed by eliminating, in reverse order, the points introduced before, using for that purpose a set of appropriate lemmas (see Fig. 5). After eliminating all the introduced points, the goal equality of the conjecture collapses to an equality between two rational expressions involving only free points. This equation can be further simplified to involve only independent variables. If the expressions on the two sides are equal, the conjecture is a theorem, otherwise it is not.

In the example above (see Theorem 1), the conjecture can be expressed using the signed area of triangles, \(\mathcal {S}_{LGK} = 0\), i.e. the signed area of the triangle LGK is zero, so we are considering a degenerate triangle, so the points are collinear. Using the area method, both GCLC and JGEX failed to prove this conjecture (only using the algebraic methods they were capable of proving it), but for the same construction the conjecture \(\overline{GK}/\overline{LG} = 2\) is provable. The proof itself is a (readable) sequence of steps preforming algebraic simplifications, geometric simplifications and the application of lemmas allowing to eliminate the free points, but with 169 pages this formal proof cannot be considered readable (see Fig. 5).

The GATP implementing these methods are efficient and capable of producing formal, but readable (in some cases, small) proofs. Given the fact that these methods do not use the usual axioms systems used in secondary schools, the proofs produced are readable, even by secondary schools’ students and teachers, but not without a previous study of the axiom system used by the GATP.

2.4 Generic First-Order Provers

First-order ATP must also be considered. Provers like Vampire, Leo and many othersFootnote 5 are very efficientFootnote 6 and capable of proving theorems in many areas. Using axioms systems for geometry, e.g. Tarski, they can be used in geometry also. For example, the Thousands of Problems for Theorem Provers (TPTP) repository (Sutcliffe, 2017) has the GEO domain with many problems specified in the first-order logic (FOL), using the Tarski Geometry (Quaife, 1989) or the geometric deductive database method (GDDM) (Chou et al., 2000)Footnote 7 axiom systems. The proof of those conjectures can then be attempted by the different ATP.

For example, the Euler’s line theorem can be expressed in the following form (using the GDDM):

figure c

the specification of the problem is done in First-Order Form (FOF). Using the ATP Vampire, the conjecture is proved by refutation; below an excerpt of the proof is given:

figure d

Using this approach, the proof script (if any) would be a logical proof (e.g. using the resolution method). As can be seen above, in the case of the proof done by the ATP Vampire, the proof contains information about the lemmas used and, if some post-processing is used, can be readable, but the connection with the geometric construction is difficult, at best.

An advantage of this approach is the availability of many generic ATPs with very efficient implementations.Footnote 8 The unavailability of geometric proofs is the drawback.

2.5 Other Approaches

Rule-based approaches explore the possibility of building a sound, not necessarily complete, axiom system. The idea is to have a minimal set of axioms, lemmas and rules of inference that can characterize a given sub-area of geometry (Pambuccian, 2004).

One example of such an approach is given by the tutorial system QED-tutrix. Exploring the logic programming language PrologFootnote 9 (Clocksin & Mellish, 2003) a set of axioms, lemmas and rules of inference, adapted to the type of problems at hand, are implemented and explored by the Prolog rule-based logical query mechanism. The QED-tutrix tutorial system builds the Hypothesis, Properties, Definitions, Intermediate results and Conclusion graph (HPDIC-graph). The HPDIC-graph contains all possible proofs for a given problem, using a given set of axioms. Having that (possibly, very large) graph the system can help the learner, validating the steps already taken and providing hints for the next steps (Font et al., 2018; Gagnon et al., 2017).

A project, still in its early stages, uses MaudeFootnote 10 (Clavel et al., 2007), an equational (and rewriting) logic system to implement the Tarski axiom system as described by Art Quaife (1989) (see Fig. 6).

Fig. 6
figure 6

Implementation, as a Maude module, of Tarski axiom system, as described by Art Quaife

Full size image

Both approaches share the use of logic programming languages where the introduction of specific lemmas, for specific purposes, can be easily made, e.g. SSS, SAS, ASA and AAS lemmas for the congruence of triangles, or the alternate interior and exterior angles of parallel lines.

As stated above, this systems can be used to implement sound, but not necessarily complete, axiom systems. These kind of system can be useful in specific situations, e.g. in secondary schools mathematics classes.

3 Dynamic Geometry

Dynamic Geometry Systems

Dynamic geometry can be characterized by the construction of geometric figures (as opposed of fixed drawings), built from free objects, i.e. universally quantified objects (e.g. points) and elementary properties preserving constructions.

Analysing the example given in Fig. 7, the construction has A, B, D and E as free points, these can be moved freely in the plane, points C and F belongs to AB and DE, respectively, they have only one degree of freedom, being able to move in the line they belong and, finally, points G, H and I are the intersections of two lines, they do not have any degree of freedom.

Fig. 7
figure 7

Pappus’ Hexagon Theorem, DGS construction

Full size image

Dynamic geometry systems give us the profane side of proofs in the Cartesian model of Euclidean geometry. By moving the free points, we can conjecture that the points G, H and I are collinear (red line), i.e. we are exploring “all” possible configurations for that geometric construction. Although these manipulations are not formal proofs because only a finite set of positions are considered and because visualisation can be misleading, they provide a first clue to the truthfulness of a given geometric conjecture.

Dynamic geometry systems are now mature software tools with a very large users base. The dynamic character of these programs give to its users the possibility of building dynamic geometric constructions, exploring conjectures about them, so they give a first, informal, opportunity to explore geometric proofs. But to avoid the visual proofs pitfall, the connection with geometric automated theorem provers (GATP) should be considered.

Dynamic Geometry Systems and Geometry Automated Theorem Provers

There are already some systems combining DGS and GATP. The following list is organized as follows: from GATP and GATP with rendering capabilities to DGS with some automatic proving capabilities built-in, ending with environments with DGS and/or GATP capabilities.  

Open Geometry Prover:

The Open Geometry Prover (OGP) is an open source project,Footnote 11 aiming to implement various geometry automated theorem provers. It can be used as a stand-alone tool but can also be integrated into other geometry tools, such as dynamic geometry software. In its current state, OGP implements the Wu’s algebraic methods. Some partial work has been made in the semi-synthetic methods: the area method and the full-angle method (Baeta & Quaresma, 2013; Botana et al., 2015; Petrović et al., 2012).

GCLC:

Geometry Constructions \(\rightarrow \) LaTeX Converter (GCLC), an open source GATP with a graphics engine, for the Wu, Gröbner bases and area methods. It is possible to add a conjecture to a given geometric construction (with a graphical rendering) and ask for its proof with natural language rendering (Janičić, 2006).

JGEX:

Java Geometry Expert (JGEX), a GATP with graphics engine, for the Wu, Gröbner bases, area, full-angle and deductive database methods. It is possible to add a conjecture to a given geometric construction and ask for its proof with natural and visual language renderings (Ye et al., 2011).

Cinderella:

The Interactive Geometry Software Cinderella is a DGS with a randomized theorem checker (Kortenkamp & Richter-Gebert, 2004; Richter-Gebert & Kortenkamp, 1999).

 

The last one has a different approach from the first three, it is not a prover capable of a formal proof, but more a model checker, capable of generating many random instances for a given geometric configuration. So, for a given conjecture, we obtain a probabilistic answer to its validity (Kortenkamp & Richter-Gebert, 2004).

Apart from the library OGP, these systemsFootnote 12 are monolith systems, i.e. even if the GATP are modules that can be used by themselves (e.g. the GCLC), the DGS and the GATP are tightly integrated. The DGS are not able to use external GATP and the GATP are not prepared to be integrated in other DGS.

A modular approach is beginning to make its way, i.e. an approach where DGS and GATP can be developed by different teams and nevertheless be combined. Examples of such systems are:  

GeoProof:

A DGS that interfaces with the Coq Prover Assistant (Bertot & Castéran, 2004), allowing to check proofs built interactively (Narboux, 2007).

GeoGebra:

The DGS embedded prover system chooses one of the available methods and translates the problem specified by the end user as the input for the selected method, similarly to portfolio solvers.Footnote 13 The available GATP implement the Wu’s method, the Buchberger–Kapur method, the area method and Recio’s exact check method. The separation between the GATP and the DGS opens the possibility of using third-party GATP. For example, the Open Geometry Prover Wu’s method GATP. From the DGS interface the user can ask for the validation of a given geometric conjecture, related to the construction, e.g. Prove AreCollinear(G, H, I) is the command that a user may use to prove, formally, that the points G, H and I in the construction of Fig. 7 are collinear. For the moment, this is only a formal validation, no proof script is available (Botana et al., 2015; Kovács, 2015; Kovács & Recio, 2020; Nikolić et al., 2019).

This project can be visited at https://www.geogebra.org/m/McEqwQNb.

 

When applied to areas such as education GATP and DGS are being combined in environments that use both tools for the purpose of learning.  

QED-Tutrix:

QED-Tutrix is an intelligent tutor for geometry (see Sect. 2.5) offering an interface to help high school students to freely explore the geometric problems and their proofs.

For each geometric conjecture, the system builds the tree of all possible proofs, allowing the students to try to prove the conjecture, with the system helping in each step of the proof (Font et al., 2018; Gagnon et al., 2017).

Geometriagon:

GeometriagonFootnote 14 is a project to explore geometric constructions made with ruler and compass. The dynamic geometry software supporting the project is C.a.R.Footnote 15 It provides an extensive list of problems to be solved by registered users, validating (or not) the solution found.

 

A similar approach, not in the area of geometry, is given by Edukera,Footnote 16 a Web-environment to teach Logic and Mathematics (calculus and sets), with the assistance of the Coq proof assistant.

4 Other Lines of Research

The usefulness of automated deduction methods and tools in geometry does not circumscribe itself to its use in dynamic geometry systems:  

Repositories of Geometric Knowledge:

 In the repository Thousand of Geometric problems for geometric Theorem Provers (TGTP),Footnote 17 a list of more than two hundred geometric conjectures and their proofs by several GATP are kept (Quaresma, 2011). It implements a protocol for the exchange of geometric information between applications, allowing a direct access to its repository from external tools.

In the repository Thousands of Problems for Theorem Provers (TPTP) (Sutcliffe, 2017),Footnote 18 a section is dedicated to geometric problems (in this repository the problems are specified as first order logic problems).

Recent efforts are being made to start a Geometry Automated Provers Competition (Baeta et al., 2020), in order to help improve the efficiency and usefulness of GATP.

Knowledge Management:

Besides the efforts to implement readable formal proofs produced by GATP, there are other avenues of research that are being explored. For example: to evaluate the complexity and also the interestingness of geometric proofs (Gao et al., 2019; Quaresma et al., 2020);Footnote 19 to explore the automatic discovery of theorems in elementary geometry (Recio & Vélez, 1999); to implement a semantic geometric search mechanism, i.e. the possibility of, having a given geometric construction, to search for other congruent geometric constructions or even other geometric constructions with some common geometric properties. A prototype of this search mechanism is already implemented in the TGTP repository (Haralambous & Quaresma, 2014, 2018).

  All these efforts are being made to help answer the questions related to the use of GATP as one more tool in the geometer’s toolbox.

5 Conclusions

It is clear that automated deduction methods and tools are beginning to make their way into many different uses, in many different contexts. However, there are many issues to be solved before a more complete integration of automated deductive tools can take place. Examples of problems related with the use of automated deduction in geometry tools are: application programming interface; common formats for information interchange; natural and visual languages renderings of the proofs; repositories of geometric knowledge with powerful search mechanisms; proof discovery; problems and proof classification for complexity and efficiency.

The complexity and the sheer size of the task led to recent efforts to establish a network of researchers working in the area of formal reasoning, knowledge-based intelligent software and geometric knowledge management. The network will need to focus in the creation of an intelligent computational environment in which advanced software tools and deduction mechanisms are embedded for symbolic-numeric geometric computation, interactive or automated geometric reasoning, knowledge validation, knowledge discovery and knowledge management. Such a “superset of a book” of geometric knowledge with embedded tools, freely available in all computational platforms, adaptable, collaborative and adaptive to each and every user’s profiles, would bring together a whole new generation of mathematical tools with impact at all levels: exploratory research, applications in mathematics and education.

All these efforts are leading to an integration of formal deduction and dynamic geometry in vivid environments, to be used in the exploration of mathematics in its fullness. It is a complex task, but it is also an exciting task, as new advances in many areas are expected in the near future.