This page is here to collect our thoughts about a joint project around dynamic geometry, proofs and constructions. This is a draft under construction which collects ideas for cooperation initiated at Castro Urdiales in February 2010.

Motivations

Technological tools are widely used to teach mathematics in schools. Dynamic Geometry Software (DGS) and Computer Algebra Software (CAS) are the two families of software that are well represented. These tools are widely used to explore, experiment, visualize, calculate, measure, find counter examples, conjecture... but most of them can not be used directly to build or check a proof.

Proof is a crucial aspect of mathematics and therefore should be integrated more into the mathematical tools. However the status of proof in the education and the impact of dynamic geometry software on the teaching of geometry and more precisely on the proving activity is a well addressed issue in the literature (See for example Furinghetti, F. & Paoloa Domingo (2003), de Villiers (1990)). In Furinghetti, F. & Paoloa Domingo (2003), the authors “confirm the interlacement of exploration and proof”. We think that these two activities could better interlaced if they were both conducted using the computer. The idea collected here are driven by the motivation to bring together dynamic geometry systems and various aspects of computer-aided theorem proving. We think that both worlds have their individual strengths (appealing visualisation and rigorisity respectively) which could benefit to each other.

So these webpages address software eliciting interest in and satisfying curiosity for the principles of mathematics and their beauty, and since anyone knows that essential insights cannot be scheduled for a certain lesson at high school, we can conclude:

The envisaged software shall cover a wide range of functionality.

In order to gain wide usage for such software, it also should support mathematics as is at schools today.

State of the art

Terminology

DGS	Dynamic Geometry System
CAS	Computer Algebra System
ATP	Automatic Theorem Proving
ITP	Interactive Theorem Proving
CTP	Computer Theorem proving (ATP+ITP)
IDE	Integrated Development Environment
MMA	Mechanised Mathematics Assistant
RP	Repository of Theorems

comment (PQ): shouldn't be RP - Repository of Problems instead of Repository of Theorems? for once the RP will match the words (or we should change it to RT), and the repository of problems will strees the fact that we may have open problems also.

DGS Dynamic Geometry Software

Dynamic Geometry Software are tools which allow to create and then manipulate geometric constructions.

ATP Automated Theorem Proving

Automated theorem provers a software system which given a statement can tell if the statement is true or not. Some ATP can produce a proof of the statement.

ITP Interactive Theorem Proving

A proof assistant is a software which can be used to interactively build a formal proof. This object is then mechanically checked by the machine. In each of these systems the user has to first define what he wants to prove and then guide the software until it accepts the proof as a valid proof. Proof assistants are different from theorem provers: proof assistants are designed for an interactive use whereas theorem provers a build to find proofs automatically. However also proof assistants usually include automation: decision procedures for particular problems as well as heuristic proof search methods.

With respect to educational use ITP's emphasis for comprehensibility by humans is important: in order to have human readable proofs, also the underlying knowledge, axioms and definitions, need to be human readable. This is accomplished best by LCF-style provers like Coq or Isabelle.

Mechanised Mathematics Assistant

Regarding the variety of concepts and technologies discussed in this wiki one might expect a conglomeration of different pieces of software. Quite in contrary, our goal is unifying the technologies in one Mathematics Assistant (MA), which is general enough to include algebra as well --- general as, for instance, underlying tools like Isabelle or Coq.

Existing systems and their capabilities

The vision is that we integrate existing systems rather than starting from scratch. For convenience we give here a list of systems which could be involved. This list is not supposed to be a final decision, just an enumeration of candidates which we deem suitable according to our current knowledge and are represented to a certain extent among the authors; other suitable systems may be added accordingly, while not all systems listed here may turn out to be really suitable in the end.

Existing systems

DGS

GeoGebra
Cinderella
GCLC Sect.
…

ITP

Coq
Isabelle^[1], Mizar, HOL, …
Isac ^[2]
…

RP

TGTP/GeoThms
…

Automatic deduction in geometry

The main methods for automated deduction in geometry are:

Gröbner basis
Wu's method
Area Method
Full-angle method
Geometric algebra

Proof discovery

Contraint Solving

Problems

Roughly speaking, geometric constraints solving consists in producing geometric figures satisfying a specification. This specification can be given under the form of a geometric statement, in the education domain, or a dimensioned sketch, in the CAD domain.

Example of a geometric statement:

Let two parallel lines, D1 and D2 be given, A and B be two points on D1 and D2   
respectively, and O be another point. Construct two points, Z1 and Z2 
respectively on D1 and D2 such that AZ1+ AZ2 = k where k is a given non  
negative number.

Example of a dimensioned sketch:

From a logical point of view, such a statement is a <math>\forall \exists</math>-formula and solving a geometric constraint system consists in yielding

either a model of the statement, also called a witness or a solution, for this formula (such a model usually is a numerical figure),
or, in education domain, a way to construct all the solutions in all the cases, that is, a geometric construction program.

In the following, we focus on the second aspect.

Automatic generation of geometric construction programs

Progé by Pascal Schreck, ...

Geometric construction language

GCL

Tutoring in stepwise construction

The introduction stresses the role of proof as 'a crucial aspect of mathematics', and addresses the importance of 'interlacements of exploration and proof'.

However, an educational context makes clear, that proof is a highly elaborated concept comprehensible only togehter with concepts like axiom, theorem etc. So there are good reasons, that high schools precede proving with another entry point to geometry:

Stepwise construction of figures is how children first encounter geometry, using paper and pencil or a DGS. Such construction problems provide the possibility of active learning, of learning by trial and error, while intuitively convincing feedback by the figure is guaranteed.

Thus we stress the demand of software, which supports stepwise constructions in geometry and proving.

Support for construction implies efficient and highly mechanised user guidance -- such kind of tutoring has not yet been realised by any system, it poses a challenging issue for our considerations here. Mechanised generation of user guidance might start from programs in a high-level language addressed above, coded by hand or generated automatically.

The experimental tutoring system ISAC employs a new technology ^[3] for user guidance in stepwise construction of calculations in applied mathematics --- together with a discussion, how this technology could be transferred from algebra to geometry.

Remarkable in the context of these webpages is, that the design of such a tutoring system raises challenges for ATP and ITP, which are discussed below.

Interactive proof in geometry

Geometry Tutor, Déﬁ (Desmoulins 94) (Anderson et al. 85) (Baulac et Giorgiutti 91)
Cabri-Euclide, Chypre (Laborde 95,Sutherland 63,Luengo 97,Bernat 94).
Mentoniezh (Dominique Py) is based on an expert module i.e. an automated theorem prover which calculates beforehand many different proofs for the statement.
Baghera is a multi-agent system for learning in geometry.

A very well develloped software for interactive proof in geometry is Geometrix

It allows both:

contruction exercises and
proof exercises

Interactive formal proof in geometry

Interactive formal proof in geometry has been studied by Frédérique Guilhot who developped a large amount of highschool geometry using the Coq proof assistant.

Automated formal proofs in geometry

There has been a lot of efforts invested in automated theorem provers in geometry and also in developing collections of formalized geometry knowledge. But, it is still to develop systems that automatically generate formal proofs. Also, it would be welcome to develop systems that automatically generate synthetic (hopefully readable) proofs of geometry conjectures. One option is to use coherent logic as a framework for that (Janicic 2010).

Some ADG methods have been formalized in ITP.

the Area Method in Coq (Narboux 2004, Narboux 2010)
the Gröbner basis method in Coq (Pottier 2008^[4])
to be completed

The recently emerged connection of ITPs to ATPs for proof search under the brand sledgehammer ^[5] could also turn out helpful.

Human-readable interactive formal proofs

In the early days of interactive theorem proving, the task of writing »proofs« meant to write down so-called tactic scripts which consisted of a programmatic combination of so-called tactics of which each would implement a particular proof strategy. This was successful but turned out to be inconvenient: tactic scripts seldom resemble the abstract human-invented ideas behind a proof, are brittle, and always refer to an implicit goal state which is not represented in the script itself, making maintenance difficult. To overcome this, declarative proof languages were developed,

starting with the Mizar system^[6]
and later on the proof languages Isar for Isabelle^[7]
and C-zar for Coq^[8].

The core idea is that instead of writing a programmatic description how to accomplish a proof, the proof writer gives a proof text describing what to prove in each step, where each step needs to be justified by either a subproof or a terminal tactical proof. This means a proof writer is free to express his ideas about the proof in his text such that a reader can follow his thoughts accordingly.

This is interesting in our context because such proof languages allow for fine-granular control while still be able to integrate automatic proof procedures. For example, in the Isar framework, the fundamental single proof step is resolution with natural deduction rules. Any proven theorem can again be used as natural deduction rule. Consequently, if domain-specific proof steps can be encoded into natural deduction rules, they can be applied directly within Isar. Beside that the system provides generic proof tools (called methods) which can instantiated for particular domains: induction (for higher-order natural deduction rules), simplification (equational rewriting with equalities), classical reasoning. Especially the two latter help to avoid spelling out proof parts explicitly which are considered trivial by the human reader.

Database of geometry problems

Geothms - GeoThms is a web-based framework for exploring geometrical knowledge that integrates Dynamic Geometry Software (DGS), Automatic Theorem Provers (ATP), and a repository of geometrical constructions, ﬁgures and proofs. The GeoThms users can easily use/browse through existing geometrical content and build new contents. In this paper we describe GeoThms functionalities, focusing on the interface solutions required for a system aimed at supporting studying and teaching geometry via Internet. GeoThms is a publicly accessible system with a growing body of geometrical constructions and formally proven geometrical theorems ^[9].

TGTP (Thousands of Geometric problems for geometric Theorem Provers) is a system aiming to support the testing and evaluation of geometric automated theorem proving (GATP) systems, to help ensure that performance results accurately reflect the capabilities of the GATP system being considered ^[10].

Proof document model

A recent developement in ITP user interfaces could have beneficial impact on our aims: a model for proof documents ^[11]. It is motivated by the observation that typical ITP systems barely provide support for contemporary editing technology and it would be waste of resources to build editors from scratch. Therefore it is proposed to design ITP systems in a way that they can interact with existing editor frameworks. One should refrain from the temptation to model arbitrary details of the ITP system in the user interface since this would be bare duplication with all negative effects like keeping versions consistent etc. Instead the interaction between ITP system and user interface is kept to a simple document model which supports basic activities like open new document, insert document fragment, drop document fragment, conclude document etc. The ITP system judges which parts of the document are to be considered valid or not and reports on that to the user interface which visualizes this to the end user accordingly (e.g. red underlining), thus mimicking the look-and-feel of contemporary IDEs for programming languages. Hence the user interface need only the knowledge whether something is valid or not, but not why.

A concrete instance of this document model is presented using Isabelle/HOL and the JVM-based jEdit editor framework, but the ideas can be transferred to similar components.

In our scenario the visual user interface would be a DGS. It would map actions in a geometry scenario (draw circle, connect dots, construct triangle, ...) onto changes of a underlying document; the checking is done within the ITP which gives feedback which steps are valid.

Goals and means

Goals

proof checking: produce a system which checks geometry conjectures (this would need integration of DGS and ATP)

proof discovery: produce a system which finds geometry conjectures

exercise correction: produce a system which can check if the answer to a construction exercise is correct (this can involve ATP methods embedded in ITP or not); this can be regarded a special case of the following:

exercise hints: produce a system which can help the student to stepwise build a construction, see above; this includes developing techniques to adapt the hints to the curriculum of the students.

interactive geometric proof: produce a system to build proofs in geometry interactively (this requires having ATP to ease the interactive proof, ways to visualize statements in DGS, a readable proof language, …)

problem collection: produce a database of geometry theorems with their proof and figures (starting with GeoThms).; conjectures should be accompanied by (when possible):

formal proofs (not neccesssarily automatic)
automatically generated proofs (not neccessarily formal)
dynamic figures (for different DGS)

solution collection: produce an electronic handbook (not necessarily online) about geometry integrating DGS, ITP and ATP

integrated system: design one system providing support from high-school to university: pupils doing an elementary construction should be able to ask the system for underlying knowledge, for instance the axiom system the MMA is using in this construction.

…: …

Means

Architecture vision

Interoperability between proof system and DGS

Automated deduction in geometry

Dealing with degenerated cases

Research issues raised by tutoring

The tutoring technology of Lucas-Interpretation (LucIn) combines computation and deduction such that this section is closely related to many other sections here.

TODO

Examples: tutoring by Lucas-interpreter

These examples shall provide concrete material for discussion. The collection of examples might be extended during the course of discussion.

Circumcenter of a triangle

The construction of a circle, which contains all points of a given triangle, is one of the first constructions a learners encounters --- and DGS convincingly show the invariant, when dragging one of the points on the screen. Leet's discuss two appoaches:

A simple set-theoretic approach which reflects the kind of comprehension general to learners at the age of about 10 years. This example is simple such that a program for the LucIn can cope with the combinatorial explosion of similar cases, which however cannot be expected for other examples.
An approach based on the area method, which is strong enough to cope with a large class of geometry problems. This approach follows ^[12] and raises questions with respect to ATP.

Since the area method is not always close to human readable proofs, other approaches might emerge during discussions here, probably using more 'traditional axioms' ^[13] restricted to Euclidean plane.

Midpoint using the butterfly theorem