Automated Theory Formation in Mathematics

Abstract

A program called is described which cairies on simple mathematics research: defining, and studying new concepts under the guidance of a large body of heuiistic rules. The 250 heurKtus communicate via an agenda mechanism, a global priority queue of small bisk', for the program to perform and teasons why each task is plausible (e.g., Find PENCRAHZTION. of 'prnes', because turued out to be so useful a Concept). Each concept is an active, structured knowledge module. One bundled very incomplete modules are initially supplied, each one corresponding to an elementary set theoretic concept (e.g., union). This provides a definite but immense space which AM begins to explore. In one boor, AM rediscovers hundreds of common concepts (including singleton sets, natural numbers, arithmetic) and theorems (e.g., unique factorization).