From: minsky@media.mit.edu Subject: Re: Mathematics trivia questions Date: Fri, 24 Dec 1999 18:25:35 GMT Newsgroups: sci.math Keywords: automated proof of Pons Asinorum In article <3862701C.43ECFE17@athensgroup.com>, Mike Christie wrote: > I believe the answer is that Euclid proved the theorem known as Pons > Asinorum and Epicurus named it. I believe the theorem is that an > isosceles triangle has equal angles opposite the equal sides because > isosceles triangles are congruent > to their mirror images. > > If that's the right connection, here's a follow-up (though I'm not > completely sure of the details here): why is it noteworthy that Marvin > Minsky proved this theorem in 1956? The point wasn't that I proved it but that my program found that proof by itself. In 1956 I wrote two memos about a hand-simulated program for proving theorems in geometry. In the first memo, the procedure found the simple proof that if a triangle has two equal sides then the corresponding angles are equal. It did this by noticing that triangle ABC was congruent to triangle CBA because of "side-angle-side". What was interesting is that this was found after a very short search—because, after all, there weren't many things to do. You might say the program was too stupid to do what a person might do, that is, think, "Oh, those are both the same triangle. Surely no good could come from giving it two different names." (The program has a collection of heuristic methods for proving Euclid-Like theorems, and one was that 'if you want to prove two angles are equal, show that they're corresponding parts of congruent triangles. Then it also had several ways to demonstrate congruence. There wasn't much more in that first simulation.) But I can't find that memo anywhere. I explained the heuristic geometry proof methods to Nathaniel Rochester at IBM research, and he set a young mathematician, Herbert Gelernter, to work on Geometry Theorem Proving. The results of this were published around 1960, I think, in the IBM Journal of Research and Development The second memo was about how to make such a program use diagrams for reasoning. It pointed out that if you conjecture a theorem, and then construct a diagram to illustrate it (using random numbers for each unconstrained variable), then the theorem will be true (with probability 1) if and only if the diagram can be constructed. That way, the program could search for diagrams augmented with construction lines. I can't find that memo either. I hope some copies still exist. Possibly John McCarthy at Stanford might have them. A few years later William A. Martin, a student of mine at MIT, was writing a program to recognize equivalent expressions in a compiler for algebraic calculations. I pointed out to him that if you had, say, the two expressions sin(2x) and 2sin(x)cos(x) these would have the same values for any random x, and that in our 64-bit machine, it would otherwise be highly improbable for any two non-equivalent expressions to have the same values for several such assignments. Martin extended this idea to invent some ingenious "symmetrical invariant hash code " methods to simplify mathematical expressions. He mapped elementary algebraic and exponential function expressions into large finite fields. It's in his Ph.D thesis around 1965 at MIT. My (simulated) program was unable to find a proof for "If a triangle has two equal angle bisectors, then the triangle is isoceles." I don't think I've ever seen a short clear proof. Sent via Deja.com http://www.deja.com/ Before you buy. ============================================================================== [These are the MathSciNet listings for Gelernter. Note that several of his papers were reproduced in the 1983 collection, Automation of reasoning. (2 volumes) MR 84f:03011a,b Classical papers on computational logic, 1957--1967. Edited by Joerg Siekmann and Graham Wrightson. Springer-Verlag, Berlin-New York, 1983. 525+637 pp. ISBN 3-540-12043-2, 3-540-12044-0 [1] 33 #3485 Gelernter, H. L. Machine-generated problem-solving graphs. 1965 Colloq. Found. Math., Math. Machines and Appl. (Tihany, 1962) pp. 283--307 Akad. Kiad, Budapest (Reviewer: S. Amarel) 68.00 [2] 29 #5410 Gelernter, Herbert Machine-generated problem-solving graphs. 1963 Proc. Sympos. Math. Theory of Automata (New York, 1962) pp. 179--203 Polytechnic Press of Polytechnic Inst. of Brooklyn, Brooklyn, N.Y. (Reviewer: A. P. Ershov) 68.00 [3] 26 #5769 Gelernter, Herbert A note on the system requirements of a digital computer for the manipulation of list structures. IRE Trans. EC-10 1961 484--489. 68.00 [4] 26 #4915 Gelernter, H. Realization of a geometry theorem proving machine. 1960 Information processing pp. 273--282 UNESCO, Paris; R. Oldenbourg, Munich; Butterworths, London 02.54 [5] 23 #B3114 Gelernter, H. L.; Rochester, N. Intelligent behavior in problem-solving machines. IBM J. Res. Develop. 2 1958 336--345. (Reviewer: H. Simon) 68.00 [6] 23 #B1083 Gelernter, H. L.; Rochester, N. Intelligent behavior in problem-solving machines. Nuovo Cimento (10) 13 1959 supplemento, 474--493. (Reviewer: H. A. Simon) 92.50 [7] 21 #3946 Gelernter, H. A note on syntactic symmetry and the manipulation of formal systems by machine. Information and Control 2 1959 80--89. (Reviewer: J. McCarthy) 68.00 (02.00) As for "Pons Asinorum", Coxeter (Introduction to Geometry, Wiley, 1980) gives this as one of his very first results. Following an apt quote from Charles Dodgson he writes, "1.5 The angles at the base of an isosceles triangel are equal. The name pos asinorum for this famous theorem probably arose from the bridgelike apearance of Euclid's figure (with the construction lines required in his rather complicated proof) and from the notion that anyone unable to cross this bridge must be an ass. Fortunately a far simpler proof was supplied by Pappus of Alexandria about 340A.D. [There is a figure]: Let ABC be an isosceles triangle with AB equal to AC. Let us conceive this triangle as two triangles and argue in this way. Since AB=AC and AC=AB, the two sides AB,AC are equal to the two sides AC,AB. Also the angle BAC is equal to the angle CAB, for it is the same. Therefore, all the corresponding parts (of the triangles ABC, ACB) are equal. In particular, < ABC = < ACB." --djr]