Proving Statements in Planar Geometry and Cinderella

This report describes the things done in a three month internship at the Technische Universität Berlin, performed in the summer of 2003. The main goal of this internship was to make it possible to put forward a geometrical theorem (i.e. a theorem involving points, lines, conics, incidences, etc) on a computer by pointing and clicking, and then obtain a computer-generated proof for this theorem. This goal was achieved, adding various options to the computer program Cinderella[4]. With Cinderella one can create geometrical configurations, and the internal ‘Randomized prover ’ is able to discover theorems. In this internship we added the functionality to find proofs for these theorems with the aid of the computer algebra package GAP[20]. Communication between these two programs and the various steps in generating the proof is done by means of OpenMath [12, 15]. Cinderella is now able to generate a mathematically correct proof of certain theorems created by the user. Moreover, one can verify this proof without extensive knowledge of the way the proof was obtained. As this internship was performe