From: Bill Dubuque Subject: Re: Geometric theorem-provers (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 over-estimating 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 e-mail. 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 so-called "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 well-known 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