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.
Why it matters
For the first time a machine proved theorems not of logic but of school geometry, using a diagram as a person does. The idea that a model of the situation tells which steps are worth trying, and the problem of auxiliary constructions, lead from this machine to AlphaGeometry in 2024.
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. What the record does not claim: how many minutes a problem took, which the 1960 paper does not say; or the days of the 1959 Paris paper, which was not read.