From: Bill Dubuque
Subject: Re: Geometric theoremprovers (Was Re: Geometry puzzle)
Date: 08 Mar 1999 02:33:03 0500
Newsgroups: sci.math
Keywords: Automatically generated proofs
The following message is a courtesy copy of an article
that has been posted as well.
Dave Rusin wrote:

 Clive Tooth wrote:
 >
 > Prof. Honsberger, having failed to find a geometrical solution, says:
 >
 > "Of course, there is always a chance that there exists an elusive
 > construction line which will make everything clear. Finding Euclidean
 > geometry so attractive, I am always reluctant to throw in the towel on
 > the synthetic approach; however, after several looks at the problem from
 > this point of view, I turned to the analytic approach."
 >
 > He then gives a "coordinate geometry" solution.

 A mathematician understands the distinction instinctively, although it's
 not really clear what the technical difference is (particularly in a problem
 like this one, with no variable elements) since locating a point with
 coordinates is equivalent to locating it by a comparison to other lengths
 and angles. So I understand there's a lame answer to my question, but:
 How effectively may one prove geometric theorems automatically?

 I haven't kept abreast of the work on automated reasoning (even right down
 the highway from me at Argonne labs) but I was sort of under the impression
 that it was nowadays reasonable to expect machines to be able to prove
 results such as this one. A scan of the links known to me showed fewer
 applications to geometry than I thought. Am I overestimating current
 progress? Pointers, anyone?
One such pointer may be found below.
From: Bill Dubuque
Subject: Re: Geometrical "proof"
Newsgroups: sci.math.research
Date: 02 Aug 1997 18:10:13 0400
tors@math.uio.no (Thor Sandmel) writes:

 I remember having seen a "proof" that all triangles are isosceles, but now
 I cannot find it. Anybody got a reference? Other examples of geometrical
 "proofs" made incorrect by improper reference to a figure are also welcome
 (but they must be short and simple). Grateful for any hint. Please respond
 by email.
See Section 7.5 (A Commentary on Proof by Picture) of H. Stark's
"An Introduction to Number Theory", where he "proves" that every
triangle is equilateral and every angle is zero. This section is
a comment on his use of pictures in his geometric approach to
continued fractions.
Note that there are methods of (synthetic) proof that are
independent of diagrams and order (e.g. the socalled "area
method"). Recently these have been employed by those working
in the automated theorem proving community with spectacular
success, e.g. see the following web page for pointers to
literature and software http://www.cs.twsu.edu/~chou
The software generates succinct readable synthetic proofs for
most wellknown geometry theorems involving lines and circles
(e.g. theorems of Desargues, Pappus, Simson, Butterfly, Feuerbach,
Fundamental Principle of Affine and Projective Geometry, etc).
Usually the proofs are competitive with human generated proofs,
and sometimes they are better! Further, they can generate
multiple different proofs, and a database of facts pertaining
to a diagram, etc. They expect that their software should
prove very useful for educational purposes, and results so far
would seem to support their claims.
Many of the automatic generated proofs are for nontrivial
problems, e.g. see the automatic proof of the Five Circle
problem that was proposed by Elkies on sci.math (Jnl. Autom.
Reas. 17 1996 p. 359), problem 10317 of the AMM 1993 (ibid
p. 366), a problem from a 1984 IMO (ibid p. 368). It is claimed
that Chinese students participating in the IMO have been trained
in such methods and that this is part of the reason for their
recent successes.
Bill Dubuque
= http://www.dejanews.com/getdoc.xp?AN=262017970