The idea of using a computer program to help discover theorems is an old one and will not surprise anyone nowadays. In late 1950s, logician Hao Wang at IBM
wrote a code called Program II (Wang 1960) to discover deep
theorems in propositional logic. For Wang, a theorem is deep
if it is short but requires a long proof. Understandably,
Wang’s program did not produce any really deep theorems,
perhaps for the simple reason that there are no tautologies
that are short and require a long proof.
A better-known example in AI is the Automated Mathematician (AM) that Douglas Lenat developed in 1976 as part
of his PhD dissertation (Lenat 1979). While not strictly about
discovering theorems, AM uses heuristic search to simulate
how mathematicians discover interesting concepts and conjectures in number theory. It caused some excitement in the
community as Lenet claimed that one of the Lisp functions
it generated represented the fundamental theorem of arithmetic.
n This article describes a framework
for machine theorem discovery and
illustrates its use in discovering state
invariants in planning domains and
properties about Nash equilibria in
game theory. It also discusses its potential use in program verification in software engineering. The main message of
the article is that many AI problems can
and should be formulated as machine
theorem discovery tasks.