{simonco, bundy}<0dai. ed. ac. uk

The HR program forms concepts and makes conjectures in domains of pure mathematics and uses theorem prover OTTER and model generator MACE to prove or disprove the con-jectures. HR measures properties of concepts and assesses the theorems and proofs involving them to estimate the interestingness of each concept and employ a best first search. This approach has led HR to the discovery of inter-esting new mathematics and enables it to build theories from just the axioms of finite algebras. 1 In t roduc t ion The HR program invents definitions in finite algebras such as group and ring theory, and other areas of pure mathematics, such as graph and number theory. Using a set of production rules to derive a new concept from old ones and a set of measures for the interestingness of a concept, HR's best first search bases new concepts on the most interesting old ones. As it invents new defin-itions, HR uses empirical evidence to spot conjectures. Recently we have interfaced HR with the OTTER the-orem prover, [McCune, 1990], to prove some of the con-jectures HR makes. When OTTER fails, HR invokes the MACE model finder, [McCune, 1994], to find a counter-example. The proofs from OTTER help HR to assess the concepts involved in the conjectures, and the mod-els given by MACE provide further empirical evidence for future conjectures. This closes a cycle of mathemat-ical activity similar in nature to Buchberger's spiral of creativity, [Buchberger, 1993]. We detail how HR forms and assesses concepts and discuss how this has led to the introduction of new mathematics. We also show how a theory can be constructed from just the axioms of an al-gebra, and how the heuristic search improves the overall quality of the theory with respect to various measures. 1.1 Background Lenat, in [Lenat, 1976] chose pure mathematics as the domain for his AM program to demonstrate the use of heuristic search in concept formation. AM re-invented classically interesting definitions and conjectures, suc