GeoProver - A Small Package for
Mechanized (Plane) Geometry Manipulations
Author: Hans-Gert Grbe

Version 1.3

Hans-Gert Grbe, Univ.  Leipzig, Inst. f. Informatik, D-04109 Leipzig, Germany

January 18, 2003

Initialization

This worksheet requires

>	restart:with(Groebner):

>	read("GeoProver.mpl"): with(geoprover): with(plots):

>	setoptions(axes=NONE,scaling=constrained):

Warning, the name changecoords has been redefined

All computations in this worksheet were tested with Maple 8.

>

1 Introduction   

Geometry is not only a part of mathematics with ancient roots but also a vivid area of modern research.  Especially the field of geometry, called by some negligence "elementary", continues to attract the attention also of the great community of leisure mathematicians. This is probably due to the small set of prerequisites necessary to formulate the problems posed in this area and the erudition and non formal approaches ubiquitously needed to solve them.  Examples from this area are also an indispensable component of high school mathematical competitions of different levels upto the International Mathematics Olympiad (IMO) [7].

     The great range of ideas involved in elementary geometry theorem proving inspired mathematicians to search for a common toolbox that allows to discover such geometric statements or, at least, to prove them in a more unified way.  These attempts again may be traced back until ancient times, e.g., to Euclid and his axiomatic approach to geometry.

     Axiomatic approaches are mainly directed towards the introduction of coordinates that allow to quantify geometric statements and to use the full power of algebraic and even analytic arguments to prove geometry theorems.  Different ways of axiomatization lead to different, even non-commutative, rings of scalars, the basic domain of coordinate values, see [9].

     Taking rational, real or even complex coordinates for granted (as we will do in the following) it turns out that geometry theorems may be classified due to their symmetry group as statements in, e.g., projective, affine or Euclidean (Cartesian) geometry.  Below such a distinction will be important for the freedom to choose appropriate coordinate systems.  

     It may be surprising that tedious but mostly straightforward manipulations of the algebraic counterparts of geometric statements allow to prove many theorems in geometry with even ingenious "true geometric" proofs.  This was already pointed out by Hilbert for configurations of points and lines. Many geometry theorems admit such proof schemes of constructive type.  

   With the help of a Computer Algebra System supporting algebraic manipulations this approach obtains new power. The method is not automatic, since one often needs a good feeling how to encode a problem efficiently into a proof scheme, but mechanized in the sense that one can develop a tool box to support proof scheme evaluation and some very standard tools to derive a (mathematically strong !)  proof from these encoded data.

     The attempts to mechanize this part of mathematics found their first culmination in the 80's in the work of W.-T. Wu [9] on "the Chinese Prover" and the fundamental book [2] of S.-C.  Chou who proved 512 geometry theorems with this method. In the 90-th the area quickly evolved with a series of conferences [1] and text books [4,8,9].

     Since the geometric interpretation of algebraic expressions depends heavily on the properties of the field of scalars, we get another classification of geometry theorems: Those with coordinate version valid over the algebraically closed field C  and those with coordinate version valid (or may be even formulated) only over R .  The latter statements include ordered geometry, that uses the distinction between "inside" and "outside", since C  doesn't admit monotone orderings.  

     The GeoProver package   provides the casual user with a couple of procedures to run geometric proof schemes written along the rules of the GeoCode standard, fixed in the GeoCode  table of the SymbolicData Data Collection, see http://www.symbolicdata.org.

Together with the  normal function for rational expressions, the solve function, and the utilities collected in the Groebner package one can prove a wide range of theorems of unordered geometry, see the examples below, the test file GeoProver.tst and the   GEO proof scheme collection of the SymbolicData Project.

     This package grew up from a course of lectures for students of computer science on this topic held by the author at the Univ.  of Leipzig in fall 1996 and was updated after a similar lecture in spring 1998.  Since 1999 versions of this package for MuPAD, Reduce, ans Mathematica are available. For versions1.2 and 1.3. the syntax was  redesigned and enhanced. The current version 1.3 implements the GeoCode standard 1.3.

2 Mechanizing Geometry Proving   

Most geometric statements are of the following form:  

Given certain (more or less) arbitrarily chosen points and/or lines we construct certain derived points and lines from them.  Then the (relative) position of these geometric objects is of a certain specific kind regardless of the (absolute) position of the chosen data.  

     To obtain evidence for such a statement (recommended before attempting to prove it !)  one makes usually one or several drawings, choosing the independent data appropriately and constructing the dependent ones out of them (best with ruler and compass, if possible). A computer may be helpful in such a task, since the constructions are purely algorithmic and computers are best suited for algorithmic tasks.  Given appropriate data structures such construction steps may be encoded into functions that afterwards need only to be called with appropriate parameters.

     Even more general statements may be transformed into such a form and must be transformed to create drawings.  This may sometimes involve constructions that can't be executed with ruler and compass as, e.g., angle trisection in Morley's theorem or construction of a conic in Pascal's theorem.    

2.1 Algorithmization of (plane) geometry  

The representation of geometric objects through coordinates is best suited for both compact (finite) data encoding and regeometrization of derived objects, e.g., through graphic output.  Note that the target language for realization of these ideas on a computer can be almost every computer language and is not restricted to those supporting symbolic computations.  Different geometric objects may be collected into a scene.  Rapid graphic output of such a scene with different parameters may be collected into animations or even interactive drag-and-move pictures if supported by the programming system. ( Geometry  offers a scratch implementation of scenes that may be plotted.)  

     We will demonstrate this approach on geometric objects, containing points and lines, represented as pairs P:Point=(p1,p2)   or tripels g:Line=(g1,g2,g3)  of a certain basic type Scalar , e.g., floating point reals.  Here g  represents the homogeneous coordinates of the line

{(x, y) : }.  

In this setting geometric constructions may be understood as functions constructing new geometric objects from given ones.  Implementing such functions variables occur in a natural way as formal parameters that are assigned with special values of the correct type during execution.  

     1) For example, the equation      

  

of the line through two given points    yields the function  

pp_line(P,Q:Point):Line  ==  (q2 - p2, p1 - q1, p2*q1 - p1*q2)  

that returns the (representation of the) line through these two points.  In this function P and Q are neither special nor general points but formal parameters of type Point.

 

     2) The (coordinates of the) intersection point of two lines may be computed solving the corresponding system of linear equations.  We get a partially defined function, since there is no or a not uniquely defined intersection point, if the two lines are parallel.  In this case our function terminates with an error message.  

intersection_point(a,b:Line):Point  ==

         d:=a1*b2 - a2*b1 ;

         if d = 0 then ERROR("Lines are parallel")

         else return ((a2*b3 - a3*b2)/d, (a3*b1 - a1*b3)/d)  

Again a  and b  are formal parameters, here of the type Line .

     3) In the same way we may define a line l  through a given point P  perpendicular to a second line a  as  

ortho_line(P:Point,a:Line):Line == (a2, -a1, a1*p2 - a2*p1)  

and a line through P  parallel to a  as  

par_line(P:Point,a:Line):Line == (a1, a2, -a1*p1 - a2*p2)  

     4) All functions defined so far returned objects with coordinates being rational expressions in the input parameters, thus especially well suited for algebraic manipulations.  To keep this nice property we introduce only the squared Euclidean distance  

sqrdist(P,Q:Point):Scalar == (p1 - q1)^2 + (p2 - q2)^2  

     5) Due to the relative nature of geometric statements some of the points and lines may be chosen arbitrarily or with certain restrictions.  Hence we need appropriate constructors for points and lines given by their coordinates  

Point(a,b:Scalar):Point == (a, b)

Line(a,b,c:Scalar):Line == (a, b, c)  

and also for a point on a given line.  For this purpose we provide two different functions  

line_slider(a:Line,u:Scalar):Point  ==

         if a2 = 0 then

                  if a1 = 0 then ERROR("a is not a line")

                  else return (-a3/a1, u)

         else return (u, -(a3 + a1*u)/a2)  

that chooses a point on a line   a  and  

varpoint(P,Q:Point,u:Scalar):Point == ((1-u)*a1 + u*b1, (1-u)*a2 + u*b2)  

that chooses a point on the line through two given points.  The main reason to have also the second definition is that u  has a well defined geometric meaning in this case.  For example, the midpoint  of PQ  corresponds  to  :

midpoint(P,Q:Point):Point == varpoint(P,Q,1/2)  

     6) One can compose these functions to get more complicated geometric objects as, e.g., the pedal point of a perpendicular    

pedalpoint(P:Point,a:Line):Point == intersection_point(ortho_line(P,a),a),  

the perpendicular bisector  of  BC

p_bisector(B,C:Point):Line == ortho_line(midpoint(B,C),pp_line(B,C)),  

the altitude  to BC  in the triangle ABC   

altitude(A,B,C:Point):Line == ortho_line(A,pp_line(B,C))  

and the median line   

median(A,B,C:Point):Line == pp_line(A,midPoint(B,C))  

     7) We can also test geometric conditions  to be fulfilled, e.g., whether two lines a  and b  are parallel or orthogonal  

is_parallel(a,b:Line):Boolean == (a1*b2 - a2*b1 = 0)  

resp.  

is_orthogonal(a,b:Line):Boolean == (a1*b1 + a2*b2 = 0)  

or whether a given point is on a given line  

on_line(P:Point,a:Line):Boolean == (a1*p1 + a2*p2 + a3 = 0)  

The corresponding procedures implemented in the package return the value of the expression to be equated to zero instead of a boolean.

     Even more complicated conditions may be checked as, e.g., whether three lines have a point in common or whether three points are on a common line.  For a complete collection of the available procedures we refer to the GeoProver documentation.

     Note that due to the linearity of points and lines all procedures considered so far return data with coordinates that are rational in the input parameters.  One can easily enlarge the ideas presented in this section to handle also non linear objects as circles and angles, compute intersection points of circles, tangent lines etc., if the basic domain Scalar admits to solve non-linear (mainly quadratic) equations.  Since non-linear equations usually have more than one solution, branching ideas should be incorporated, too.  For example, intersecting a circle and a line the program should consider both intersection points.    

2.2 Mechanized evidence of geometric statements  

With a computer and these prerequisites at hand one may obtain evidence of geometric statements not only from plots but also computationally, converting the statement to be checked into a function depending on the variable coordinates as parameters and plugging in different values for them.

     For example, the following function tests whether the three perpendicular bisectors in a triangle given by the coordinates of its vertices A, B, C  pass through a common point  

test(A,B,C:Point):Boolean ==

is_concurrent(p_bisector(A,B), p_bisector(B,C), p_bisector(C,A))  

Plugging in different values for A, B, C   we can verify the theorem for many different special geometric configurations.  Of course this is not yet a proof.  

     Lets add another remark: Point  and Line  are not only the basic data types of our geometry, but data type functions parametrized by the data type Scalar .  To have the full functionality of our procedures Scalar  must be a field with effective zero test.   

3 Geometry Theorems of Constructive Type   

Implementing the functions described above in a system, that admits also symbolic computations, we can execute the same computations also with symbolic values, i.e.  taking a pure transcendental extension of Q  as scalars.  The procedures then return (simplified) symbolic expressions that specialize under (almost all) substitutions of "real" values for these symbolic ones to the same values as if they were computed by the original procedures with the specialized input.  This leads to the notion of generic geometric configurations.  A geometric statement holds in this generic configuration, i.e., the corresponding symbolic expression simplifies to zero, if and only if it is "generically true", i.e., holds for all special coordinate values except degenerate ones.    

3.1 Geometric configurations of constructive type  

This approach is especially powerful, if all geometric objects involved into a configuration may be constructed step by step and have rational expressions in the algebraically independent variables as symbolic coordinates.  

      Definition:  We say that a geometric configuration is of constructive type ,  if its generic configuration may be constructed step by step in such a way, that the coordinates of each successive geometric object may be expressed as rational functions of the coordinates of objects already available or algebraically independent variables, and the conclusion may be expressed as vanishing of a rational function in the coordinates of the available geometric objects.    

Note that this notion is different from that used in [2].  

     Substituting the corresponding rational expressions of the coordinates of the involved geometric objects into the coordinate slots of newly constructed objects and finally into the conclusion expression, we obtain successively rational expressions in the given algebraically independent variables.

  

A geometry theorem of constructive type is generically true if and only if (its configuration is not contradictory and) the conclusion expression simplifies to zero.  

     Indeed, if this expression simplifies to zero, the algebraic version of the theorem will be satisfied for all "admissible" values of the parameters.  If the expression doesn't simplify to zero, the theorem fails for almost all such parameters.

     Note that due to cancelation of denominators the domain of definition of the simplified expression may be greater than the (common) domain of definition of the different parts of the unsimplified expression.  The correct non degeneracy conditions describing "admissibility" may be collected during the computation. Collecting up the zero expression indicates, that the geometric configuration is contradictory.  Hence the statement, that a certain geometric configuration of constructive type is contradictory, is of constructive type, too.

     The GeoProver  package provides procedures clear_ndg(), print_ndg()   to manage and print these non degeneracy conditions and also a procedure add_ndg(d)  as a hook for their user driven management.    

3.2 Some one line proofs  

Take independent variables  and  

>	A:=Point(a1,a2); B:=Point(b1,b2); C:=Point(c1,c2);

as the vertices of a generic triangle.  We can prove the following geometric statements about triangles computing the corresponding (compound) symbolic expressions and proving that they simplify to zero.  Note that our procedures return rational expressions already in normal form.  

1) The perpendicular bisectors of ABC  pass through a common point since  

>	is_concurrent(p_bisector(A,B), p_bisector(B,C), p_bisector(C,A));

returns zero.  

2) The intersection point of the perpendicular bisectors  

>	M:=intersection_point(p_bisector(A,B), p_bisector(B,C));

is the center of the circumscribed circle since  

>	sqrdist(M,A)-sqrdist(M,B);

simplifies to zero.  

3) Euler's line:  

The center M of the circumscribed circle, the orthocenter H and the barycenter S are collinear and S divides M H with ratio 1:2.  

Compute the coordinates of the corresponding points  

>	M:=intersection_point(p_bisector(A,B), p_bisector(B,C));

>	H:=intersection_point(altitude(A,B,C),altitude(B,C,A));

>	S:=intersection_point(median(A,B,C),median(B,C,A));

and then prove that  

>	is_collinear(M,H,S);

>	sqrdist(S,varpoint(M,H,1/3));

>

both simplify to zero.  

4) Feuerbach's circle:  

The midpoint N of MH is the center of a circle that passes through nine special points, the three pedal points of the altitudes, the midpoints of the sides of the triangle and the midpoints of the upper parts of the three altitudes.  

Due to Cartesian symmetry we may choose a special coordinate system with origin A  and (after scaling) x -axes unit point B .  The remaining point C  is arbitrary.  

>	A:=Point(0,0); B:=Point(u1,0); C:=Point(u2,u3);

and compute the coordinates for M, H , and N  

>	M:=intersection_point(p_bisector(A,B), p_bisector(B,C));

>	H:=intersection_point(altitude(A,B,C),altitude(B,C,A));

>	N:=midpoint(M,H);

Now evaluate  

>	sqrdist(N,midpoint(A,B))-sqrdist(N,midpoint(B,C));

>	sqrdist(N,midpoint(A,B))-sqrdist(N,midpoint(H,C));

>	D_:=intersection_point(pp_line(A,B),pp_line(H,C));

>	sqrdist(N,midpoint(A,B))-sqrdist(N,D_);

>

Again the last expression simplifies to zero thus proving the theorem.

Choosing special  coordinates we generate a plot of the configuration. First we arrange the different geometric figures to be plotted into different scenes. A scene  is a list of special geometric objects, i.e., a special geometric configuration.

>	A:=Point(0,0): B:=Point(10.,0): C:=Point(4.,7.):

>	scene1:=[pp_line(A,B), pp_line(B,C), pp_line(A,C)]:

>	scene2:=[altitude(A,B,C), altitude(B,C,A), altitude(C,A,B)]:

>	scene3:=[p_bisector(A,B), p_bisector(B,C), p_bisector(C,A)]:

>	scene4:=[median(A,B,C), median(B,C,A), median(C,A,B)]:

>	M:=intersection_point(p_bisector(A,B), p_bisector(B,C)):

>	H:=intersection_point(altitude(A,B,C),altitude(B,C,A)):

>	N:=midpoint(M,H):

>	scene5:=[pp_line(M,H),pc_circle(N,midpoint(A,B))]:

Now we plot all or part of the chosen geometric figures with the (undocumented GeoProver 's) geo_plot  command. It takes a scene as first argument and an expression <var>=range  that determines both the horizontal and vertical ranges of the picture as second argument. Optionally a color definition   color=<color> may be added as third argument. To plot the union of all scenes it in the standard (black) color we type

>	geo_plot([op(scene1), op(scene2), op(scene3), op(scene4), op(scene5)], x=-2..10);

Merging plots with different colors using Maple's display  command produces even more "coloured" pictures:

>	P1:=geo_plot(scene1,x=-2..10,color=green):    # the triangle

>	P2:=geo_plot(scene2,x=-2..10,color=red):       # the altitudes

>	P3:=geo_plot(scene3,x=-2..10,color=blue):      # the perpendicular bisectors

>	P4:=geo_plot(scene4,x=-2..10,color=magenta):   # the median lines

>	P5:=geo_plot(scene5,x=-2..10,color=black):     # Euler's line

>	display(P1,P2,P3,P4,P5);

>

4 Non-linear Geometric Objects   

The GeoProver   package provides several functions to handle angles and circles as non-linear geometric objects.    

4.1 Angles and bisectors  

(Oriented) angles between two given lines are presented as tangens of the difference of the corresponding slopes.  Since  

 

we get for the tangens of the angle between two lines g, h  

l2_angle(g,h:Line):Scalar == (g2*h1-g1*h2)/(g1*h1+g2*h2)  

     Note that in unordered geometry we can't distinguish between inner and outer angles.  Hence we cannot describe (rationally) the parameters of the angle bisector of a triangle.  For a point P  the equation  

l2_angle(pp_line(A,B),pp_line(P,B)) = l2_angle(pp_line(P,B),pp_line(C,B))

i.e., angle(ABP) = angle(PBC) , describes the condition to be located on either the inner or outer bisector of angle(ABC).   Clearing denominators yields a procedure   

>	A:=Point(a1,a2); B:=Point(b1,b2); C:=Point(c1,c2); P:=Point(p1,p2);

>	on_bisector(P,A,B,C);

that returns on generic input a polynomial of (total) degree 4 and quadratic in the coordinates of P  that describes the condition for P  to be on (either the inner or the outer) bisector of angle(ABC) .  

     With some more effort one can also employ such indirect geometric descriptions.  

5) For example, we can prove the following unordered version of the angle bisector intersection theorem:

There are four common points on the three angle bisector pairs of a given triangle ABC.  

Again we may choose special coordinates with two independent parameters  - the coordinates of C :  

>	A:=Point(0,0);  B:=Point(1,0);  C:=Point(u1,u2);

A point   

>	P:=Point(x1,x2);

is an intersection point of three angle bisectors iff it is a common zero of the polynomial system  

>	polys:={ on_bisector(P,A,B,C), on_bisector(P,B,C,A), on_bisector(P,C,A,B)};

with indeterminates  over the coefficient field Q ( ).  A Grbner basis computation

>	TO:=plex(x1,x2);

>	gb:=gbasis(polys,TO);

yields an equivalent system with two equations. The first equation has 4 solutions in  and each of them may be completed with a single value for  from the second equation.  Hence the system of polynomials  has four generic solutions corresponding to the four expected intersection points.  The generic solutions involve algebraic numbers of degree 4 over the generic field of scalars Q( ) as coordinates that specialize to the correct "special" intersection points for almost all values of the parameters  and .

     It is hard (and not recommended from a computational point of view) to give explicit descriptions through radicals of these symbolic values, since it is more efficient to compute with them as RootOf  expressions, i.e., knowing only their minimal polynomials.  Since in this situation  is the distance from P  to the line AB , we can prove that each of the four points has equal distance to each of the three sides of the triangle ABC , i.e., that these points are the centers of its incircle and the three excircles.  First we compute the differences of the corresponding squared distances ( srqdist_pl(P,a)==sqrdist(P,pedalpoint(P,a)) )

>	con:=[sqrdist_pl(P,pp_line(A,C))-sqrdist_pl(P,pp_line(A,B)), sqrdist_pl(P,pp_line(B,C))-sqrdist_pl(P,pp_line(A,B))];

The numerator of each of these two expressions should simplify to zero under the special algebraic values of x1, x2.  This may be verified computing their normal forms with respect to the above Grbner basis:   

>	map(u->normalf(numer(u),gb,TO),con);

>

Note that [10] proposes also a constructive proof for the angle bisector intersection theorem:

     Start with A, B  and the intersection point P  of the bisectors through A  and B .  Then g(AC)  and g(BC)  are symmetric to g(AB)  wrt. g(AP)  and g(BP)  and P  must be on their bisector:   

>	A:=Point(0,0); B:=Point(1,0); P:=Point(u1,u2);

>	l1:=pp_line(A,B);

>	l2:=sym_line(l1,pp_line(A,P));

>	l3:=sym_line(l1,pp_line(B,P));

>	on_bisector(P,A,B,intersection_point(l2,l3));

>

Again the last expression simplifies to zero and thus proves the theorem.

The four intersection points of the angle bisectors are the centers of the in- and the excircles. For a special  geometric configuration we may solve the polynomial of degree 4, obtain the coordinates of the four centers and plot the corresponding figure:

>	A:=Point(0,0); B:=Point(10.,0); C:=Point(4.,6.); P:=Point(x1,x2); Q:=Point(x1,0);

>	polys:={on_bisector(P,A,B,C), on_bisector(P,B,C,A)};

>	sol:={solve(polys,{x1,x2})};

We substitute these solution pairs into pc_circle(P,Q)

>	scene1:=map(x->subs(x,pc_circle(P,Q)),sol):

to collect the four circles. Similarly

>	scene2:=map(x->op(subs(x,[pp_line(A,P),pp_line(B,P),pp_line(C,P)])),sol):

collects the 6 different bisectors of the triangle (each twice, since it passes through 2 of the 4 excenters P) and

>	scene3:=[pp_line(A,B),pp_line(A,C),pp_line(B,C)]:

collects the sides of the triangle. Thus we finally get as plot

>	rg:= x = -12..18:

>	display(geo_plot(scene1,rg,color=blue), geo_plot(scene2,rg,color=magenta), geo_plot(scene3,rg));

>

4.2 Circles  

The GeoProver   package encodes circles through homogeneous coordinates   (k1, k2, k3, k4)  as the set of points

     k := { (x, y) : }.

This allows for denominator free representation and includes lines as special case: The line g = (g1, g2, g3)   is the circle (0, g1, g2, g3) .

     Its easy to derive formulas

circle_center(k)

for the center of the circle  k and

circle_sqradius(k)

for its squared radius .  It is also straightforward to test

on_circle(P,k).  

The parameters of the circle

p3_circle(A,B,C)

through 3 given points  

A:=Point(a1, a2); B:=Point(b1, b2); C=Point(c1, c2);  

may be obtained from a nontrivial solution of the homogeneous linear system with coefficient matrix  

 

The condition that 4 points are on a common circle then may be expressed as  

is_concyclic(A,B,C,D) == on_circle(D,p3_circle(A,B,C));  

For generic points    

>	A:=Point(a1,a2); B:=Point(b1,b2); C:=Point(c1,c2); D_:=Point(d1,d2);

this condition

>	p4:=on_circle(D_,p3_circle(A,B,C));

is a polynomial  of degree 4. The same polynomial arizes with the circular angle theorem :

>	u:=l2_angle(pp_line(A,D_),pp_line(B,D_));

>	v:=l2_angle(pp_line(A,C),pp_line(B,C));

>	w:=normal(numer(u)*denom(v)-denom(u)*numer(v));

>

w+p4;

>	u:='u':v:='v':w:='w':

Note that this condition is also equivalent to Ptolemy's theorem.

If two circles or a circle and a line have a known (rational) point P  in common the coordinates of the second intersection point Q can be computed and saved into a function other_cl_point(P,c,d)  or other_cc_point(P,c1,c2) . Conditions on the coordinates of a circle and a line resp. two circles to be tangent may be derived in a similar way.  

6) These functions admit a constructive proof of Miquels theorem :  

Let ABC be a triangle.  Fix arbitrary points P, Q, R on the sides AB, BC, AC.  Then the three circles through each vertex and the chosen points on adjacent sides pass through a common point.

   Take as above   

>	A:=Point(0,0); B:=Point(1,0); C:=Point(c1,c2);

Generic points on the sides may be introduced with three auxiliary indeterminates:   

>	P:=varpoint(A,B,u1);

>	Q:=varpoint(B,C,u2);

>	R:=varpoint(A,C,u3);

Then   

>	X:=other_cc_point(P,p3_circle(A,P,R),p3_circle(B,P,Q));

is the intersection point of two of the circles different from P  (its generic coordinates contain 182 terms) and since   

>	on_circle(X,p3_circle(C,Q,R));

>

simplifies to zero the third circle also passes through X .    

With special coordinates we may plot the figure as follows:

>	spec:={c1=0.4,c2=0.6,u1=0.423, u2=0.621, u3=0.331}:

>	scene1:=subs(spec,[pp_line(A,B), pp_line(A,C), pp_line(B,C)]):

>	scene2:=subs(spec, [p3_circle(A,P,R), p3_circle(B,P,Q), p3_circle(C,Q,R)]):

>	rg:=x=-0.25 .. 1.2:

>	display(geo_plot(scene1,rg),geo_plot(scene2,rg,color=red));

>

5 Geometry Theorems of Equational Type   

5.1 Algebraic formulation of geometric statements

As already seen in the last section non-linear geometric conditions are best given through implicit polynomial dependency relations on the coordinates of the geometric objects.  In this more general setting a geometric statement may be translated into a generic geometric configuration, involving different geometric objects with coordinates depending on (algebraically independent) variables v = ( ,..., ) , a system of polynomial conditions F  = { ,...,  }   that express the implicit geometric conditions and a polynomial   g  that encodes the geometric conclusion. Then for a certain polynomial non degeneracy condition h  the following holds:   

The geometric statement is true iff for all non degenerate correct special geometric configurations, i.e., with coordinates, obtained from the generic ones by specialization   ->   in such a way, that     for all f  \in F, but   , the conclusion holds, i.e.,     vanishes.  

Denoting by Z(F)  the set of zeroes of the polynomial system F and writing Z(h) = Z({h}) for short, we arrive at geometry theorems of equational type, that may be shortly stated in the form  

  Z(F) - Z(h) \subset    Z(g).  

Over an algebraically closed field, e.g.   C , this is equivalent to the ideal membership problem   

g * h \in rad I(F),  

where rad I(F) is the radical of the ideal generated by F .  Even if h  is unknown a detailed analysis of the different components of the ideal I(F)  yields more insight into the geometric problem.

     Note the symmetry between g  and h  in the latter formulation of geometry theorems.  This shows that non degeneracy conditions for a given geometry theorem of equational type may be obtained from the stable ideal quotient  

h \in rad I(F) : g^ \infty.  

Since every element of this ideal may serve as non degeneracy condition there is no weakest condition among them, if the ideal is not principal.    

5.2 Dependent and independent variables  

Let  S = R[ ,..., ] be the polynomial ring in the given variables over the field of scalars R.   The polynomial system F describes algebraic dependency relations between these variables in such a way that the values of some of the variables may be chosen (almost) arbitrarily whereas the remaining variables are determined upto a finite number of values by these choices.  

     A set of variables u subset v is called independent   wrt.  the ideal  I = I(F) iff

I*R[u] = (0),

 i.e., the variables are algebraically independent modulo I.  If u is a maximal subset with this property the remaining variables x = v \ u are called dependent.

     Although a maximal set of independent variables may be read off from a Grbner basis of I  there is often a natural choice of dependent and independent variables induced from the geometric problem.   u  is a maximal independent set of variables iff F has a finite number of solutions as polynomial system in x  over the generic scalar field R(u) .  In many cases this may be proved with less effort than computing a Groebner basis of I over S .

     If F  has an infinite number of solutions then u  was independent but not maximal.  If F  has no solution then u  was not independent.    

5.3 Geometry theorems of linear type  

We arrive at a particularly nice situation in the case when F  is a non degenerate quadratic linear system of equations in x  over R(u) .  Such geometry theorems are called of linear type.

     In this case there is a unique (rational) solution x = x(u)  that may be substituted for the dependent variables into the geometric conclusion g = g(x, u) .  As for geometry theorems of constructive type we get a rational expression in u  such that

the geometry theorem holds (under the non degeneracy condition  in R[u], where  is the determinant of the linear system F) iff this expression simplifies to zero.  

7) As an example consider the theorem of Pappus :  

Let A, B, C and P, Q, R be two triples of collinear points.  Then the intersection points g(AQ)^g(BP), g(AR)^g(CP) and g(BR)^g(CQ) are collinear.

  The geometric conditions put no restrictions on A, B, P, Q and one restriction on each C  and R .  Hence we may take as generic coordinates   

>	A:=Point(u1,u2);  B:=Point(u3,u4);  C:=Point(x1,u5);

>	P:=Point(u6,u7);  Q:=Point(u8,u9);  R:=Point(u0,x2);

with   u0 ,..., u9   independent and x1, x2 dependent, as polynomial conditions   

>	polys:={is_collinear(A,B,C), is_collinear(P,Q,R)};

and as conclusion   

>	con:=is_collinear( intersection_point(pp_line(A,Q),pp_line(P,B)), intersection_point(pp_line(A,R),pp_line(P,C)), intersection_point(pp_line(B,R),pp_line(Q,C)));

This is a rational expression with many terms.  The polynomial conditions are linear in x1, x2  and already separated.  Hence   

>	sol:=solve(polys,{x1,x2});

>	normal(subs(sol,con));

>

proves the theorem since the expression obtained from con substituting the dependent variables by their rational expressions in u simplifies to zero.

  Here is a picture of the geometric configuration under consideration:

>	A:=Point(1,1):  B:=Point(2,2):  C:=Point(4,4):  P:=Point(1,0):  Q:=Point(2,0):  R:=Point(3,0):

>	scene1:=[pp_line(A,C), pp_line(P,R)]:

>	scene2:=[pp_line(A,Q), pp_line(P,B), pp_line(A,R), pp_line(P,C), pp_line(B,R), pp_line(Q,C)]:

>	scene3:=[ pp_line(intersection_point(pp_line(A,R),pp_line(P,C)), intersection_point(pp_line(B,R),pp_line(Q,C)))]:

>	rg:=x=-0.1..4.1:

>	display(geo_plot(scene1,rg),geo_plot(scene2,rg,color=green),geo_plot(scene3,rg,color=red));

>

As for most theorems of linear type the linear system may be solved "geometrically" and the whole theorem may be translated into a constructive geometric statement:   

>	A:=Point(u1,u2);  B:=Point(u3,u4);  P:=Point(u6,u7);  Q:=Point(u8,u9);

>	C:=varpoint(A,B,u5);

>	R:=varpoint(P,Q,u10);

>	is_collinear( intersection_point(pp_line(A,Q),pp_line(P,B)), intersection_point(pp_line(A,R),pp_line(P,C)), intersection_point(pp_line(B,R),pp_line(Q,C)));

>

5.4 Geometry theorems of non-linear type  

Lets return to the general situation of a polynomial system F \subset S that describes algebraic dependency relations, a subdivision v = x \union u  of the variables into dependent and independent ones, and the conclusion polynomial g(x, u) \in S.   The set of zeros Z(F) may be decomposed into irreducible components that correspond to prime components P_k of the ideal I = I(F) generated by F over the ring S = R[x, u].

     Since P_k \supset I the variables u may become dependent wrt. P_k. Prime components where u remains independent are called generic , the other components are called special .  Note that each special component contains a non zero polynomial in R[u].   Multiplying them all together yields a non degeneracy condition h = h(u) \in R[u] on the independent variables such that a zero c \in Z(F) with  necessarily belongs to one of the generic components.  Hence they are the "essential" components and we say that the geometry theorem is generically true, when the conclusion polynomial g vanishes on all these generic components.  

     If we compute in the ring S_0 = R(u)[x], i.e., consider the independent variables as parameters, exactly the generic components remain visible.  Indeed, this corresponds to a localization of S  by the multiplicative set R[u]\ {0}.   Hence the geometry theorem is generically true iff g \in rad(I)*S_0, i.e.   g belongs to the radical of the ideal I in this special extension of S.   A sufficient condition can be derived from a Grbner basis G of F with the u variables as parameters: Test whether

normalf(g,G,S_0) = 0,

i.e., the normal form vanishes.  More subtle examples may be analyzed with the Grbner factorizer or more advanced techniques.  

8) As an application we consider the following nice theorem from [4, ch.  4, par. 2] about Napoleon triangles :  

Let ABC be an arbitrary triangle and P, Q and R the third vertex of equilateral triangles erected externally on the sides BC, AC and AB of the triangle.  Then the lines g(AP), g(BQ) and g(CR) pass through a common point, the Fermat point  of the triangle ABC.  

     A mechanized proof again will be faced with the difficulty that unordered geometry can't distinguish between different sides wrt. a line.  A straightforward formulation of the geometric conditions starts with independent coordinates for A, B, C  and dependent coordinates for P, Q, R .  W.l.o.g.  we may fix the coordinates in the following way:   

>	A:=Point(0,0);  B:=Point(0,2);  C:=Point(u1,u2);

>	P:=Point(x1,x2);  Q:=Point(x3,x4);  R:=Point(x5,x6);

There are 6 geometric conditions ( eq_dist(A,B,C,D)==sqrdist(A,B)-sqrdist(C,D) ) for the 6 dependent variables.   

>	polys:={ eq_dist(P,B,B,C), eq_dist(P,C,B,C), eq_dist(Q,A,A,C),  eq_dist(Q,C,A,C), eq_dist(R,B,A,B), eq_dist(R,A,A,B)};

These equations may be divided into three groups of two quadratic relations for the coordinates of each of the points P, Q, R .  Each of this pairs has (only) two solutions, the inner and the outer triangle vertex, since it may easily be reduced to a quadratic and a linear equation, the line equation of the corresponding perpendicular bisector.  Hence the whole system has 8 solutions and by geometric reasons the conclusion   

>	con:=is_concurrent(pp_line(A,P), pp_line(B,Q), pp_line(C,R));

will hold on at most two of them.  Due to the special structure the interreduced polynomial system is already a Groebner basis and hence can't be split by the Groebner factorizer.  A full decomposition into isolated primes may be computed using the "projection trick", that binds an appropriate linear combination of the variables to a new variable u  and applies the Groebner factorizer to the extended system of equations with lowest variable u :   

>	polys1:=[x1+x2+x3+x4+x5+x6-u,op(polys)];

>	vars:=[x1,x2,x3,x4,x5,x6,u];

>	iso:=gsolve(polys1,vars);

This yields four components over R(u) , each corresponding to a pair of solutions over the algebraic closure.  (Note that some older Maple versions take not the prescribed term order.   In this case the following remark doesn't hold.) On precisely one of them the conclusion polynomial reduces to zero thus proving the geometry theorem.   

>	map(x->normalf(con,x[1],x[2]),[op(iso)]);

With a formulation as in [2, p. 123], that uses oriented angles, we may force all Napoleon triangles to be erected on the same side (internally resp. externally) and prove a more general theorem as above. Define a new function

eq_angle(A,B,C,P,Q,R)==p3_angle(A,B,C)-p3_angle(P,Q,R) ,

take isosceles triangles with equal base angles and (due to one more degree of freedom) x5  as independent. The conclusion remains valid:   

>	polys2:={ eq_dist(P,B,P,C), eq_dist(Q,A,Q,C), eq_dist(R,A,R,B), eq_angle(R,A,B,P,B,C), eq_angle(Q,C,A,P,B,C)};

>	sol:=solve(polys2,{x1,x2,x3,x4,x6});

>	normal(subs(sol,con));

again simplifies to zero.  Note that the new theorem is of linear type.    

>

6 More Examples   

In this section we discuss in detail some more examples and give a list of exercises.

6.1 Theorems that can be translated into theorems of constructive or linear type  

There are many geometry theorems that may be reformulated as theorems of constructive type.  

9) The affine version of Desargue's theorem:  

If two triangles ABC and RST are in similarity position, i.e., g(AB) || g(RS), g(BC) || g(ST) and g(AC) || g(RT), then g(AR), g(BS) and g(CT) pass through a common point (or are parallel).  

     The given configuration may be constructed step by step in the following way: Take A, B, C, R  arbitrarily, choose S  arbitrarily on the line through R  parallel to g(AB)  and T  as the intersection point of the lines through R  parallel to g(AC)  and through S  parallel to g(BC) .   

>	A:=Point(a1,a2); B:=Point(b1,b2);  C:=Point(c1,c2);  R:=Point(d1,d2);

>	S:=line_slider(par_line(R,pp_line(A,B)),u);

>	T:=intersection_point(par_line(R,pp_line(A,C)),par_line(S,pp_line(B,C)));

>	is_concurrent(pp_line(A,R),pp_line(B,S),pp_line(C,T));

Another proof may be obtained translating the statement into a theorem of linear type.  Since the geometric conditions put no restrictions on A, B, C, R , one restriction on S  ( g(AB) || g(RS) ) and two restrictions on T  ( g(BC) || g(ST), g(AC) || g(RT) ), we may take as generic coordinates   

>	A:=Point(u1,u2); B:=Point(u3,u4); C:=Point(u5,u6);  R:=Point(u7,u8); S:=Point(u9,x1); T:=Point(x2,x3);

with u1 ,..., u9  independent and x1, x2, x3  dependent, as polynomial conditions   

>	polys:={ is_parallel(pp_line(R,S),pp_line(A,B)), is_parallel(pp_line(S,T),pp_line(B,C)), is_parallel(pp_line(R,T),pp_line(A,C))};

and as conclusion   

>	con:=is_concurrent(pp_line(A,R),pp_line(B,S),pp_line(C,T));

The polynomial conditions are linear in x1, x2, x3  and thus   

>	sol:=solve(polys,{x1,x2,x3});

>	normal(subs(sol,con));

>

proves the theorem.

The general version of Desargue's theorem :  

The lines g(AR), g(BS) and g(CT) pass through a common point iff the intersection points g(AB)^g(RS), g(BC)^g(ST) and g(AC)^g(RT) are collinear.  

may be reduced to the above theorem by a projective transformation that  maps the line through the three intersection points to infinity. Its algebraic formulation   

>	A:=Point(0,0); B:=Point(1,0); C:=Point(u5,u6);  R:=Point(u7,u8); S:=Point(u9,u1); T:=Point(u2,x1);

>	con1:=is_collinear( intersection_point(pp_line(R,S),pp_line(A,B)), intersection_point(pp_line(S,T),pp_line(B,C)), intersection_point(pp_line(R,T),pp_line(A,C)));

>	con2:=is_concurrent(pp_line(A,R),pp_line(B,S),pp_line(C,T));

contains a polynomial con2  that is linear in x1  and a rational function con1  with a numerator that is quadratic in x1  and  factors as      

numer(con1) = u6 * con2 * is_collinear(R, S, T)  

>	normal(   numer(con1) - u6 * con2 * is_collinear(R, S, T));

This also proves the general theorem.

For a plot we choose special values for the independent variables

>	s:={u1=1.4,u2=0.6,u5=0.4,u6=0.6,u7=1.2,u8=0.8,u9=0.8};

and compute the corresponding value for the dependent variable

>	s1:=solve(subs(s,con2),{x1});

Now we collect the different parts of the scene and merge them together.

>	scene1:=subs(s,s1,[pp_line(A,B), pp_line(A,C), pp_line(B,C)]):

>	scene2:=subs(s,s1,[pp_line(R,S), pp_line(R,T), pp_line(S,T)]):

>	scene3:=subs(s,s1,[pp_line(A,R), pp_line(B,S), pp_line(C,T)]):

>	scene4:=subs(s,s1,[pp_line(intersection_point(pp_line(S,T),pp_line(B,C)), intersection_point(pp_line(R,T),pp_line(A,C)))]):

>	rg:=x=-0.2..2.2:

>

display(

geo_plot(scene1,rg),                     # triangle ABC

geo_plot(scene2,rg,color=blue),          # triangle RST

geo_plot(scene3,rg,color=green),         # the concurrent lines

geo_plot(scene4,rg,color=red));          

>

10) Consider the following theorem about Brocard points  ([2, p. 336])  

Let ABC be a triangle.  The circles c1 through A, B and tangent to g(AC), c2 through B, C and tangent to g(AB), and c3 through A, C and tangent to g(BC) pass through a common point.  

It leads to a theorem of linear type that can't be translated into constructive type in an obvious way.  The 6 circle center coordinates are defined by 6 polynomial conditions:

>	A:=Point(0,0); B:=Point(1,0); C:=Point(u1,u2);    M1:=Point(x1,x2); M2:=Point(x3,x4); M3:=Point(x5,x6); c1:=pc_circle(M1,A); c2:=pc_circle(M2,B); c3:=pc_circle(M3,C);

>	polys:={ is_cl_tangent(c1,pp_line(A,C)), on_circle(B,c1), is_cl_tangent(c2,pp_line(A,B)), on_circle(C,c2), is_cl_tangent(c3,pp_line(B,C)), on_circle(A,c3)};

that are (essentially) linear in the dependent variables.  We get rational values for the (generic) coordinates of the Borcard circle centers and prove that the intersection point of two of them is also on the third Brocard circle:  

>	vars:={x1,x2,x3,x4,x5,x6};

>	sol:=solve(polys,vars);

>	P:=other_cc_point(B,subs(sol,c1),subs(sol,c2));

>	on_circle(P,subs(sol,c3));

For a picture we specify the independent coordinates

>	s1:={u1=0.3,u2=.8};

compute the corresponding values

>	s2:=subs(s1,sol);

for the dependent coordinates and generate the parts of the plot to be constructed.

>	scene1:=subs(s1,[pp_line(A,B), pp_line(A,C), pp_line(B,C)]):

>	scene2:=subs(s1,s2,[c1,c2,c3]):

>	rg:=x=-1..2:display(geo_plot(scene1,rg), geo_plot(scene2,rg,color=red));

>

  

Even some theorems involving nonlinear objects as circles may be translated into theorems of constructive type using a rational parametrization of the non linear object.  For a circle with unit radius and center M =  ( , ) we may use the rational parametrization

{ (     ) | u \in C }

There are also more general rational parametrizations for circles with given center M and circumfere point A. This way we can prove  

11) Simson's theorem  ([1, p.  261], [4, thm.  2.51]):  

Let P be a point on the circle circumscribed to the triangle ABC and X, Y, Z the pedal points of the perpendiculars from P onto the lines passing through pairs of vertices of the triangle.  These points are collinear.  

Take the center M  of the circumscribed circle as the origin and a circumfere point A  on the x -axis.  The proof of the problem may be mechanized in the following way:  

>	M:=Point(0,0); A:=Point(r,0); B:=circle_slider(M,A,u2); C:=circle_slider(M,A,u3); P:=circle_slider(M,A,u4);

>	X:=pedalpoint(P,pp_line(A,B));

>	Y:=pedalpoint(P,pp_line(B,C));

>	Z:=pedalpoint(P,pp_line(A,C));

>	is_collinear(X,Y,Z);

This proves the theorem. Here is a picture:    

>	s:={u1=0, u2=-1., u3=1.5, u4=5.,r=1.0}:

>	scene1:=subs(s,[pp_line(A,B), pp_line(A,C), pp_line(B,C)]):

>	scene2:=subs(s,[pp_line(X,P), pp_line(Y,P), pp_line(Z,P)]):

>	scene3:=subs(s,[pc_circle(M,A)]):

>	scene4:=subs(s,[pp_line(X,Y)]):

>	rg:=x=-1.2..1.5: display(geo_plot(scene1,rg), geo_plot(scene2,rg,color=blue), geo_plot(scene3,rg,color=magenta), geo_plot(scene4,rg,color=red));

>

6.2 Theorems of equational type  

12) Consider the Butterfly Theorem ([1, p.  269], [4, thm.  2.81]) :  

Let A, B, C, D be four points on a circle with center O, P the intersection point of AC and BD and F resp.  G the intersection point of the line through P perpendicular to OP with AB resp.  CD.   Then P is the midpoint of FG.  

Taking P as the origin and the lines g(FG) and g(OP) as axes we get the following coordinatization:  

>	P:=Point(0,0);  O_:=Point(u1,0);

>	A:=Point(u2,u3); B:=Point(u4,x1);

>	C:=Point(x2,x3); D_:=Point(x4,x5);

>	F:=Point(0,x6);  G:=Point(0,x7);   c:=pc_circle(O_,A);

>	polys:={on_circle(B,c), on_circle(C,c), on_circle(D_,c), on_line(P,pp_line(A,C)), on_line(P,pp_line(B,D_)), on_line(F,pp_line(A,D_)), on_line(G,pp_line(B,C))};

>	con:=numer(sqrdist(P,midpoint(F,G)));

Note that the formulation of the theorem includes  and . Hence the conclusion may (and will) fail on some of the components of Z(polys).   This can be avoided supplying appropriate constraints to the Grbner factorizer:  

>	vars:=[x6,x7,x3,x5,x1,x2,x4];

>	sol:=gsolve(polys,vars,{sqrdist(A,C),sqrdist(B,D_)});

>	map(x->normalf(con,x[1],x[2]),sol);

>

sol contains a single solution.  Hence the Grbner factorizer could split off the components and remove the auxiliary ones. (Note that some older versions of Maple take a wrong term order or generate a content division error.)

To generate a picture we need some more effort. First, let's specify the  independent parameters

>	s1:={u1=1.0,u2=-0.5,u3=-0.5,u4=2.5};

Then we compute the possible values for the dependent variables. We replace the gsolve  by the solve  command:

>	sol:=[solve(subs(s1,polys),{op(vars)})];

This yields 8 solutions, but 6 of them are "wrong" since either A=C  or B=D . We remove them:

>	p1:=subs(s1,sqrdist(A,C)): p2:=subs(s1,sqrdist(B,D_)):

>	s2:=select(x->evalb(subs(x,p1)*subs(x,p2)<>0),sol);

The remaining solutions correspond to the two possible values for  if  is fixed. Now we can generate the corresponding plots:

>	scene1:=subs(s1,[p3_circle(A,B,C), pp_line(A,B), pp_line(A,C), pp_line(B,D_), pp_line(C,D_)]):

>	scene2:=[[1,0,0]]: rg:=x=-2..3.2:

>	display(geo_plot(subs(op(1,s2),scene1),rg), geo_plot(scene2,rg,color=red));

>	display(geo_plot(subs(op(2,s2),scene1),rg), geo_plot(scene2,rg,color=red));

>

     Note that there is also a constructive proof of the Butterfly theorem, see the record Butterfly_2  in the SymbolicData GEO collection.

13) Let's prove another property of Feuerbach's circle ([4, thm. 5.61]):  

For an arbitrary triangle ABC Feuerbach's circle is tangent to its in- and excircles (tangent circles for short).  

Take the same coordinates as in example 5 and construct the coordinates of the center N  of Feuerbach's circle c1  as in example 4:  

>	A:=Point(0,0);  B:=Point(2,0);  C:=Point(u1,u2);

>	M:=intersection_point(p_bisector(A,B),p_bisector(B,C));

>	H:=intersection_point(altitude(A,B,C),altitude(B,C,A));

>	N:=midpoint(M,H);

>	c1:=pc_circle(N,midpoint(A,B));

The coordinates of one of the excenters   

>	P:=Point(x1,x2);

are bound by the conditions  

>	polys:={on_bisector(P,A,B,C), on_bisector(P,B,C,A)};

The conclusion may be expressed as  

>	Q:=pedalpoint(P,pp_line(A,B)): con:=is_cc_tangent(pc_circle(P,Q),c1);

The polynomial conditions polys have four generic solutions, the centers of the four tangent circles, as derived in example 5.  A Groebner basis calculation finishes the proof:

>	TO:=plex(x1,x2);

>	gb:=gbasis(polys,TO);

>	normalf(con,gb,TO);

For a special geometric configuration one may compute the coordinates of the centers of the for tangent circles explicitely

>	s1:={u1=.5,u2=.9}:

>	s2:=[solve(subs(s1,polys),{x1,x2})];

and generate the corresponding picture

>	scene1:=subs(s1,[pp_line(A,B), pp_line(A,C), pp_line(B,C)]):    # the triangle

>	scene2:=map(x->subs(x,pc_circle(P,Q)),s2):              # the tangent circles

>	scene3:=[subs(s1,c1)]:                                  # Feuerbach's circle

>	rg:=x=-1..2.4: display(geo_plot(scene1,rg), geo_plot(scene2,rg,color=blue),  geo_plot(scene3,rg,color=green));

>

[4, ch.5, par. 6] points out that Feuerbach's circle of ABC  coincides with Feuerbach's circle of each of the triangles ABH , ACH  and BCH .  Hence there are another 12 "interesting" circles tangent to c1 .  This may be proved in just the same way.

     Note that the proof in [4] uses inversion geometry.  The author doesn't know about a really "elementary" proof of this theorem.   

7 Exercises   

• 1.  ([1, p.  267]) Let ABCD  be a square and P  a point on the line parallel to BD  through C  such that l(BD) = l(BP) , where l(BD) denotes the distance between B  and D .  Let Q be the intersection point of BF and CD .  Show that l(DP) = l(DQ) .  
• 2.   The altitudes' pedal points theorem : Let P, Q, R  be the altitudes' pedal points in the triangle ABC .  Show that the altitude through Q bisects angle(PQR) .   
• 3.  Let ABC be an arbitrary triangle.  Consider the three altitude pedal points and the pedal points of the perpendiculars from these points onto the the opposite sides of the triangle.  Show that these 6 points are on a common circle, the Taylor circle .  
• 4.  Prove the formula  
• 
• for the area of the triangle ABC , if a, b, c are the lengths of its sides and R the radius of its circumscribed circle.  
• 5.  ([1, p.  283]) Let k be a circle, A the contact point of the tangent line from a point B to k, M the midpoint of AB and D a point on k .  Let C be the second intersection point of DM with k, E the second intersection point of BD with k and F the second intersection point of BC with k .  Show that EF is parallel to AB .  
• 6.  (35th IMO 1995, Toronto, problem 1, [6]) Let A, B, C, D be four distinct points on a line, in that order.  The circles with diameters AC and BD intersect at the points X and Y .  The line XY meets BC at the point Z .  Let P be a point on the line XY different from Z .  The line CP intersects the circle with diameter AC at the points C and M , and the line BP intersects the circle with diameter BD at the points B and N .  Prove that the lines AM, DN and XY are concurrent.  
• 7.  (34th IMO 1994, Hong Kong, problem 2, [6]) ABC is an isosceles triangle with AB = AC .  Suppose that  
• (i) M is the midpoint of BC and O is the point on the line AM such that OB is perpendicular to AB ;  
• (ii) Q is an arbitrary point on the segment BC different from B and C ;  
• (iii) E  lies on the line AB and F lies on the line AC such that E, Q and F   are distinct and collinear.  
• Prove that OQ is perpendicular to EF if and only if QE = QF .  
• 8.  (4th IMO 1959, Czechia, problem 6, [7]) Show that the distance d between the centers of the inscribed and the circumscribed circles of a triangle ABC satisfies
• ,
• where r is the radius of the circumscribed circle and  the radius of the inscribed circle.  
• 9.  (1th IMO 1959, Roumania, problem 5, [7]) Let M be a point on AB, AMCD and MBEF squares to the same side of g(AB) and N the intersection point of their circumscribed circles, different from M .  
•  (i) Show that g(AF) and g(BC) intersect at N .  
• (ii) Show that all lines g(MN) for various M meet at a common point.    

8 References   

• [1]  Automated Deduction in Geometry. (Toulouse 1996, LNCS 1360; Beijing 1998, LNCS 1669; Zurich 2000, LNCS 2061)
• [2]  S.-C. Chou. Mechanical geometry theorem proving . Reidel, Dortrecht, 1988.  
• [3]  S.-C.  Chou.   Automated  reasoning  in  geometries  using  the  characteristic set method and Groebner basis method. In Proc. ISSAC-90 , pages 255-260. ACM Press, 1990.  
• [4] S.-C. Chou, X.-S. Gao, and J.-Z. Zhang. Machine proofs in geometry , volume 6 of the Series on Applied
    Mathematics . World Scientific, Singapore, 1994.
• [5]  H.S.M. Coxeter and S.L. Greitzer. Geometry revisted . Random House, The L.W. Singer Comp., New York, 1967.
• [6]  H.-G. Grbe: Cali - A Reduce Package for Commutative Algebra. Version 2.2.1, 1995
• [7]  The International Mathematical Olympiads, since 1959. See, e.g. John Scholes IMO page (http://www.kalva.demon.co.uk/imo.html)
• [8]  W.-T. Wu. Mathematics Mechanization , volume 489 of Mathematics and its Applications . Science Press, Beijing, and Kluwer Acad. Publ., Dordrecht, 2000.
  [9] W.-T. Wu. Mechanical Theorem Proving in Geometries . Number 1 in Texts and Monographs in Symbolic Computation. Springer, Wien, 1994.