Fifth Central- and Eastern European Conference
on Computer Algebra- and Dynamic Geometry Systems
in Mathematics Education

We discuss a new approach to didactics of mathematics triggered by technological innovation: Computer Theorem Proving (TP) attains increasing attention by application to large proofs, for instance to the Kepler conjecture. On the other hand, respective technology is still open source and used in several prototypes. Possible kinds of interaction in such prototypes is compared with possible interaction in chess software (where the latter usually is not TP-based).

Given TP-based educational software and the context of a problem in applied mathematics, then each input of the player/learner is checked reliably by the system (a move of a certain figure to a certain field on the chessboard / a formula or method promoting a calculation within the given context); and if the player gets stuck, the system can propose a next step (a move towards winning the game / a formula or method solving the problem at hand). The result of the interaction between learner and system on the screen is expected to be close to what is written on paper during an examination on applied mathematics.

The didactical analysis, which will be given for the above software-based approach, does not emphasize the fun of playing; rather, the strengths of reliability and of variability supported by TP technology will be emphasized: If an input is wrong, the system will state the incorrectness with the reliability of formal logic (while variants are handled with maximal generosity); explanations, of what is wrong in detail, can be given from TP-technology's feature of transparency. The variability of interaction follows from TP-technology’s power: if the learner is not satisfied with the progress of a calculation, she or he can go back a few steps and try another way. Or one can explore variants by going to different intermediate states and watch the system trying a solution.

The paper shows what a qualitative change in the effective use of proof is brought by contemporary mathematical software in the teaching of mathematics. Particular corresponding examples of school practice are presented. Such use of mathematical software, however, makes new demands on the teachers. They must for example choose suitable topics, adapt the lesson organization, change teaching methods and methods of evaluation. The paper brings the first results of the research that was done by the first author Irena Štrausová which focused on the role of the teacher when teaching mathematics using dynamic visual proofs at selected secondary schools.

Proving facts in school geometry involves several processes, among others: sketching, observing, stating hypothesis, checking them, and providing deductive argumentation. Nowadays technology provides considerable support to some of these processes, in particular dynamic geometry software is a valuable aid for sketching geometric configurations and empirical checking hypotheses. Currently, considerable effort is put into developing systems for automated proving.

In the presentation we shall explore the role of automated observation, i.e. using technology to detect properties of dynamic constructions. Observation is an essential part of analysis of a construction and enables the generation of hypotheses that possibly lead to synthetic or simple algebraic proofs. Automated observation is not only a powerful ‘geometric eye’ that spots hardly perceptible properties, it also gives rise to new ‘obstacles' in geometric thinking and calls for specific demands on dynamic geometry software. In this sense we shall present some solutions that are implemented in OK Geometry software. One of them, the implicit constructions, allows that geometric objects (in a dynamic construction) are specified by required properties and not (entirely) by construction steps. Automated observation of implicit construction may bring to light properties that lead to the solution of a problem related to the studied configuration.

Perhaps the most promising potential related to automated observation is the use of a database of (dynamic) geometric objects and operations. We shall present the implementation of a database related to the geometry of triangle, consisting of several thousands of characteristic points of a triangle (e.g. incentre, orthocentre), known as Kimberling centres, and a large number of lines, circles, conics, and geometric operations; many of these objects possess interesting geometric properties. In this way automated observation does not take into account only the objects of a studied construction but as well tries to relate them to the objects in the database.