Hao Wang: Principia in minutes
In January 1960 Hao Wang described in the IBM Journal programs for the IBM 704 that proved over 200 theorems of the propositional calculus from the first five chapters of Principia Mathematica in under 3 minutes of proving time, and 139 of 158 theorems from its predicate part. He wrote the programs in the summer of 1958 at IBM's Poughkeepsie laboratory.
Why it matters
Chapters of Principia that Logic Theorist had handled by heuristics and only in part, a complete algorithmic procedure worked through entirely in minutes. Wang himself sets this against the heuristic approach of Newell, Shaw and Simon: from here on machine proof has two paths, heuristic search and complete methods.
The whole propositional run took about 37 minutes, but 12/13 of the time went on input and printing. The 52 theorems Newell, Shaw and Simon had chosen were proved in under 5 minutes. Of the theorems *9 to *13 of the predicate calculus with equality, 158 in all, Program III as it stood proved 139; in a note added in proof on 10 November 1959 Wang reports that an improved program proved all 158 in about four minutes. What the record does not claim: Wang's affiliation at the time of publication; the byline gives none, and the text says the work was done at the IBM laboratory.