Theorem Proving Machine
A theorem-proving machine is a program built to discover or check mathematical proofs without a human choosing each step, and the term belongs above all to the first decade of computing, when proving theorems seemed like the purest test of machine intelligence. Between 1954 and 1965 four separate lines of work appeared, each attacking the problem differently: decision procedures, heuristic imitation of human reasoning, exhaustive systematic search, and finally the unifying idea of resolution. The later field of automated reasoning, and the existing glossary entry on theorem proving, treat the broader and more modern subject; this entry is about the early machines.
The first program that proved anything was Martin Davis's implementation of Presburger arithmetic in 1954, run at the Institute for Advanced Study in Princeton. Presburger arithmetic, the theory of the natural numbers with addition but not multiplication, had been shown decidable by Mojżesz Presburger in 1929, so Davis's program carried out a known algorithm rather than anything resembling insight. It still counts as a milestone because it showed that a stored-program computer could handle quantified statements, and it was reported to prove a simple result such as the sum of two even numbers being even. The contrast with later efforts is instructive: a decision procedure guarantees an answer, but only for a narrow, tame theory.
Logic Theorist, written in 1955-56 by Allen Newell, Cliff Shaw and Herbert Simon, took the opposite path and tried to prove theorems the way a person would, by heuristic search. Working with Whitehead and Russell's Principia Mathematica, it started from the axioms and applied substitution, detachment and replacement rules, using methods to choose promising subgoals instead of enumerating everything. It proved 38 of the first 52 theorems in chapter 2 of Principia, and for at least one theorem found a shorter proof than the book's. It was demonstrated at the 1956 Dartmouth summer project and is often called the first artificial intelligence program, though that title is argued over, and its significance lies as much in the list-processing languages and the heuristic-search idea that it inspired.
Hao Wang's 1958-60 program showed that brute force with good organization could beat heuristics on the same material. Wang, a logician then working at IBM, used an approach based on a sequent-style calculus and ran it on an IBM 704, where it proved the propositional theorems of Principia and large numbers of predicate-calculus theorems in a few minutes of machine time. His published paper, "Toward Mechanical Mathematics," argued in effect that Logic Theorist had been solving a problem that did not need heuristics, and that the human-style search of the AI school was an unnecessary detour for this logic. The dispute between the heuristic and the algorithmic camp, between mimicking mathematicians and exploiting machine speed, has recurred in every generation of the field.
Herbert Gelernter's geometry machine, described in 1959 and reported with Hansen and Loveland in 1960, added the key idea that a program could use a semantic model to prune its own search. It worked on plane geometry on the IBM 704 and used a diagram, stored as coordinates, to reject subgoals that were false in the figure, a bit like a student glancing at a sketch to avoid chasing impossible claims. Because most false subgoals fail in the diagram, the search tree shrank dramatically, and the program solved problems from high-school-level geometry texts. The same principle of using a model to filter candidates reappears in modern solvers and in neural-guided proof search, where a learned model plays the role of the diagram.
The line that most shaped the future ran through Davis and Putnam's 1960 procedure and Robinson's 1965 resolution principle, which replaced hand-tuned heuristics with a single complete inference rule. Resolution, with its unification algorithm, made first-order proof search uniform and complete, though it was famously prone to combinatorial explosion, so that research since has gone into strategies, term indexing and clause selection. Interactive systems grew up alongside: de Bruijn's Automath in the late 1960s, Milner's LCF in the 1970s, and then Coq and Lean, in which a human guides the proof and a small trusted kernel checks every step. Large machine-checked developments, such as the mathematics library built around Lean, descend from this lineage, and neural models now suggest tactics to such systems.
A frequent misconception is that these early programs were nearly human-level mathematicians; in fact they handled textbook-scale theorems in narrow domains, and the combinatorial explosion kept them there. A second is that proof by machine is untrustworthy: a proof checked by a small kernel is often more reliable than a long human argument.
Read the theorem-proving machine as the first laboratory where reasoning was turned into search: its four early programs split into decide, imitate, enumerate and unify, and the questions they raised about heuristics versus systematic completeness still shape every modern prover.