Gelernter's machine proves geometry theorems

In early spring 1959 an IBM 704 at the IBM Research Center, running a program of some 20,000 instructions, proved its first theorem of Euclidean plane geometry. Herbert Gelernter's machine accepted a subgoal only if it held in the diagram, and so rejected false steps before trying to prove them.

According to the 1960 paper by Gelernter, Hansen and Loveland, without the diagram the program generated about 1,000 subgoals per stage, and with it accepted 5 on average; the diagram check, the authors say, could never produce a false proof. The program was written in a list-processing language compiled by FORTRAN; more than fifty proofs were on file when the paper was written. Gelernter and Rochester had described the plan in 1958 as a consequence of the Dartmouth project; in October 1958, by their paper, the program was still being written (p. 342) and the geometer was being studied by simulation on the IBM 704 (p. 344). Gelernter's paper at the Paris conference (Proceedings of the International Conference on Information Processing, UNESCO, Paris, 15-20 June 1959, pp. 273-282) was read in two ways: in full in the chapter of Computers and Thought (Feigenbaum and Feldman, 1963, pp. 134-152) that reprints it, and only through full-text search passages in a lending copy of the proceedings, whose pages were not viewed. The chapter is not word for word the paper: it says the long-range research program was established at the IBM Research Center in New York, while the search passage from the paper's first paragraph (p. 273; the start of the sentence is cut off) says that a first objective has been attained, in the simulation on a high-speed digital computer of a machine capable of discovering proofs in plane geometry. The paper calls the geometry machine a particular state configuration of the IBM 704, as does the chapter (p. 139). Its proof transcripts end in total times of 0.32, 4.06, 8.08 ("with basic heuristics") and 1.06 ("with extended heuristics"; the chapter, with the same transcripts, prints the unit as minutes). The chapter prints them as three appendices. Appendix A, a point on the bisector of an angle is equidistant from its sides: 0.32 minute; the text says less than a minute. Appendix B, a quadrilateral with one pair of opposite sides equal and parallel: at 0.88 minute the machine prints "I am stuck", constructs the auxiliary segment DB, restarts and finishes at 4.06; the text says less than five minutes. Appendix C, two vertices of a triangle are equidistant from the median to the side they determine, run twice: 8.08 minutes with basic heuristics, 1.06 with extended. By the text (p. 145) the basic heuristics took about eight minutes, twenty-four circuits of the subgoal loop, sixty-one intermediate subgoals and a graph twelve levels deep; the extended ones one minute, four circuits, twenty-one subgoals and three levels. The other timings have no transcript: a Brooklyn technical high school final examination problem, under five minutes with extended heuristics while the basic ones exhausted working storage in half an hour (also in the search passage of the paper, p. 279); the diagonals of a parallelogram, about three minutes in either mode; another such problem, eight minutes against three. The day of the talk. In the printed programme of the conference (UNESCO Handbook, pp. 28-29) Gelernter's paper, "Realization of a geometry theorem proving machine", stands on Friday 19 June 1959, in the afternoon (3 to 6 p.m.), in Session I, "Session on Proving of Logical Propositions", third of five, between Gilmore and Dunham with his co-authors. UNESCO document NS/155 (Annex III, pp. 8-9; undated on the pages read) and the conference Journal's lists of chairmen (chairman I. I. Basilovsky, vice-chairman S. N. Alexander) give the same Friday and session. This is a forward schedule (the Handbook before the conference, the Journal in its first days), not a report of what happened: no document read gives the hour of the talk, the Journals read announce no change to Session I, Journal No. 5, presumably the Friday issue, was not seen, and the order of chapters in the proceedings, by its preface, is not that of the meetings. What the record does not claim: that the month or day of the first proof is known. No document read names one; there is only "early spring 1959" in the 1960 paper. The talk's scheduled day, 19 June, is not the date of the first proof. The 20,000 instructions and "early spring" are found only in the first paragraph of the 1960 paper (in its 1963 reprint, p. 153, citing 1959b, which the book's bibliography, p. 490, titles as the Paris paper); they are in neither the book chapter of the 1959 paper (pp. 134-152) nor, by search in the recognised text of the Internet Archive copy, pp. 273-282 of the proceedings; but the pages of the original were not viewed, so there the absence rests on search, and the chapter is not a copy. Which transcript answers which problem, and the figures of the text of p. 145, were read only in the chapter, not on the pages of the paper. The first printing of the 1960 paper, as read earlier, gives no time per problem; its 1963 reprint prints transcripts with times of 1.03, 8.12 ("I am stuck") and 30.68 minutes (pp. 161, 163).