The problem of automated theorem finding

This article is the twenty-fifth of a series of articles discussing various open research problems in automated reasoning. The problem proposed for research asks one to identify appropriate properties to permit an automated reasoning program tofind new and interesting theorems, in contrast toproving conjectured theorems. Such programs are now functioning in many domains as valuable reasoning assistants. A sharp increase in their value would occur if they could also be used as colleagues to (so to speak) produce research on their own.This work was supported by the Office of Scientific Computing, U.S. Department of Energy, under Contract W-31-109-Eng-38.