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]