Boyer and Moore: induction without human hints
In August 1973, at IJCAI in Stanford, Robert Boyer and J Strother Moore of the University of Edinburgh described a program that proves theorems about recursive LISP functions by mathematical induction on its own; among them, that REVERSE is its own inverse and that a particular sorting program is correct. On an ICL 4130 each theorem took 8 seconds on average.
Why it matters
The machine built the induction formula itself for functions it had not seen before: according to the paper, the user supplies the function definitions and nothing more. Proving a program correct, a sort for instance, became a task for the machine with no human hint.
The program takes a LISP expression, runs it in an interpreter and derives an induction formula from the way the interpreter fails; to this it adds simple rewrite rules of LISP and a heuristic for generalising the theorem. According to the paper, the user supplies nothing but the function definitions. The 8-second average was measured on an ICL 4130 in POP-2. Appendix B lists the theorems proved. What the record does not claim: how many theorems the appendix holds; the paper does not count them.