Empirical explorations of the geometry theorem machine

Abstract

In early spring, 1959, an IBM 704 computer, with the assistance of a program comprising some 20 000 individual instructions, proved its first theorem in elementary Euclidean plane geometry. Since that time, the geometry theorem-proving machine (a particular state configuration of the IBM 704 specified by the afore-mentioned machine code) has found solutions to a large number of problems taken from high school textbooks and final examinations in plane geometry. Some of these problems would be considered quite difficult by the average high school student. In fact, it is doubtful whether any but the brightest students could have produced a solution for any of the latter group when granted the same amount of prior "training" afforded the geometry machine (i.e., the same vocabulary of geometric concepts and the same stock of previously proved theorems).