FOM: Are machines better in math?

[Jesse Alama]

On Thu, Feb 21, 2002 at 11:14:47AM +0000, Roger Bishop Jones wrote:

> [snip]
> 
> I think the most relevant Argonne work is with the Otter resolution theorem
> prover which does proof by reductio absurdum.

Otter is an instance of a class of theorem-provers that exploit the
so-called resolution principle, first formulated by Robinson ("A
machine-oriented logic based on the resolution principle", Journal of
the ACM, 12(1):23-41, January 1965).  The resolution principle
asserts, in its simplest form, that from the propositions (A or ~B)
and B, the proposition A can be inferred.  Theorem provers that employ
Robinson's resolution principle often proceed by reductio ad
absurdum.

> This can find proofs of interesting and previously unproven mathematical
> results, but the discovery is of the proof, not of the result.
> I don't think there is any problem in getting similar technology to
> "discover" new theorems, but some difficulty in selecting what is
> "interesting" without human intervention.

Indeed, the automatic discovery of theorems has been a fruitful area
of research in artificial intelligence.  In the late 1970's, the
computer scientist Douglas Lenat designed a computer program called
AM, which stands for Automated Mathematician.  AM was successful in
applying heuristics and automated theorem-proving techniques to aid in
the discovery of new theorems.  Some of AM's results are quite
surprising and interesting.  See Lenat's "Automated theory formation
in mathematics", Proceedings of the Fifth International Joint
Conference on Artificial Intelligence (pp. 833-- 842).



Jesse