Automated Theory Formation in Pure Mathematics

In recent years, Artificial Intelligence researchers have largely focused their efforts on solving specific problems, with less emphasis on 'the big picture' - automating large scale tasks which require human-level intelligence to undertake. The subject of this book, automated theory formation in mathematics, is such a large scale task. Automated theory formation requires the invention of new concepts, the calculating of examples, the making of conjectures and the proving of theorems. This book, representing four years of PhD work by Dr. Simon Colton demonstrates how theory formation can be automated. Building on over 20 years of research into constructing an automated mathematician carried out in Professor Alan Bundy's mathematical reasoning group in Edinburgh, Dr. Colton has implemented the HR system as a solution to the problem of forming theories by computer. HR uses various pieces of mathematical software, including automated theorem provers, model generators and databases, to build a theory from the bare minimum of information - the axioms of a domain. The main application of this work has been mathematical discovery, and HR has had many successes. In particular, it has invented 20 new types of number of sufficient interest to be accepted into the Encyclopaedia of Integer Sequences, a repository of over 60,000 sequences contributed by many (human) mathematicians.

1. Introduction.- 1.1 Motivation.- 1.2 Aims of the Project.- 1.3 Contributions.- 1.4 Organisation of the Book.- 1.5 Summary.- 2. Literature Survey.- 2.1 Some Philosophical Issues.- 2.2 Mathematical Theory Formation Programs.- 2.2.1 The AM Program.- 2.2.2 The GT Program.- 2.2.3 The IL Program.- 2.2.4 The Bagai et al. Program.- 2.3 The BACON Programs.- 2.4 Concept Invention.- 2.4.1 The Representation of Mathematical Concepts.- 2.4.2 Inductive Logic Programming.- 2.5 Conjecture Making Programs.- 2.5.1 The Graffiti Program.- 2.5.2 The AutoGraphiX Program.- 2.5.3 The PSLQ Algorithm.- 2.6 The Otter and MACE Programs.- 2.7 The Encyclopedia of Integer Sequences.- 2.8 Summary.- 3. Mathematical Theories.- 3.1 Group Theory, Graph Theory and Number Theory.- 3.1.1 Group Theory.- 3.1.2 Graph Theory.- 3.1.3 Number Theory.- 3.1.4 Isomorphism.- 3.2 Mathematical Domains.- 3.2.1 Reasons Behind Theory Formation.- 3.2.2 Finite and Infinite Domains.- 3.3 The Content of Theories.- 3.3.1 Concepts.- 3.3.2 Conjectures, Theorems and Proofs.- 3.3.3 Other Aspects of Theories.- 3.4 Summary.- 4. Design Considerations.- 4.1 Aspects of Theory Formation.- 4.1.1 Aspects Which are Modelled.- 4.1.2 Some Aspects Which are not Modelled.- 4.2 Concept and Conjecture Making Decisions.- 4.2.1 The Use of Examples.- 4.2.2 Making Conjectures.- 4.3 The Domains HR Works in.- 4.4 Representation Issues.- 4.4.1 Examples of Concepts.- 4.4.2 Definitions of Concepts.- 4.4.3 Representation of Conjectures, Proofs and Counterexamples.- 4.5 The HR Program in Outline.- 4.6 Summary.- 5. Background Knowledge.- 5.1 Objects of Interest (Entities).- 5.2 Required Information about Concepts.- 5.3 Initial Concepts from the User.- 5.3.1 Initial Concepts in Graph Theory.- 5.3.2 Initial Concepts in Number Theory.- 5.3.3 Initial Concepts in Finite Algebraic Systems.- 5.4 Generating Initial Concepts from Axioms.- 5.5 Summary.- 6. Inventing Concepts.- 6.1 An Overview of the Production Rules.- 6.1.1 Some Common Construction Techniques.- 6.2 The Exists Production Rule.- 6.2.1 Data Table Construction and Parameterisations.- 6.2.2 Generation of Definitions.- 6.3 The Match Production Rule.- 6.3.1 Data Table Construction and Parameterisations.- 6.3.2 Generation of Definitions.- 6.4 The Negate Production Rule.- 6.4.1 Data Table Construction and Parameterisations.- 6.4.2 Generation of Definitions.- 6.5 The Size Production Rule.- 6.5.1 Data Table Construction and Parameterisation.- 6.5.2 Generation of Definitions.- 6.6 The Split Production Rule.- 6.6.1 Data Table Construction and Parameterisations.- 6.6.2 Generation of Definitions.- 6.7 The Compose Production Rule.- 6.7.1 Data Table Construction and Parameterisations.- 6.7.2 Generation of Definitions.- 6.7.3 Generalisation of Previous Production Rules.- 6.8 The Forall Production Rule.- 6.8.1 Data Table Construction and Parameterisations.- 6.8.2 Generation of Definitions.- 6.9 Efficiency and Soundness Considerations.- 6.9.1 Forbidden Paths.- 6.9.2 Generated and Stored Properties.- 6.9.3 Proving Consistency Between Data Tables and Definitions.- 6.10 Example Constructions.- 6.11 Summary.- 7. Making Conjectures.- 7.1 Equivalence Conjectures.- 7.1.1 Making Equivalence Conjectures Automatically.- 7.1.2 Implementation Details.- 7.2 Implication Conjectures.- 7.2.1 Making Implication Conjectures Automatically.- 7.2.2 Implementation Details.- 7.3 Non-existence Conjectures.- 7.3.1 Making Non-existence Conjectures Automatically.- 7.4 Applicability Conjectures.- 7.4.1 Making Applicability Conjectures Automatically.- 7.4.2 Implementation Details.- 7.5 Conjecture Making Using the Encyclopedia of Integer Sequences.- 7.5.1 Presenting Concepts as Integer Sequences.- 7.5.2 Conjecture Types.- 7.5.3 Pruning Methods.- 7.5.4 An Example Conjecture.- 7.6 Issues in Automated Conjecture Making.- 7.6.1 Choice of Conjecture Making Techniques.- 7.6.2 When to Check for Conjectures.- 7.6.3 The Use of Data and Pruning Methods.- 7.6.4 Other Conjecture Formats.- 7.7 Summary.- 8. Settling Conjectures.- 8.1 Reasons for Settling Conjectures.- 8.2 Proving Conjectures.- 8.2.1 Using Otter to Prove Conjectures.- 8.2.2 Sub-conjectures and Prime Implicates.- 8.2.3 Using HR to Prove Implication Conjectures.- 8.2.4 Details of HR’s Theorem Proving.- 8.2.5 Advantages of Using HR to Prove Theorems.- 8.3 Disproving Conjectures.- 8.3.1 Using MACE to Find Counterexamples.- 8.3.2 Using HR to Find Counterexamples.- 8.3.3 Finding Counterexamples in Non-algebraic Domains.- 8.4 Returning to Open Conjectures.- 8.5 Summary.- 9. Assessing Concepts.- 9.1 The Agenda Mechanism.- 9.2 The Interestingness of Mathematical Concepts.- 9.2.1 What Makes a Concept Interesting?.- 9.2.2 What Makes a Concept Uninteresting?.- 9.2.3 Interestingness Gained from Theory Formation.- 9.3 Intrinsic and Relational Measures of Concepts.- 9.3.1 Comprehensibility.- 9.3.2 Parsimony.- 9.3.3 Applicability.- 9.3.4 Novelty.- 9.4 Utilitarian Properties of Concepts.- 9.4.1 Productivity.- 9.4.2 Classification Tasks.- 9.5 Conjectures about Concepts.- 9.6 Details of the Heuristic Searches.- 9.6.1 When and How to Measure Concepts.- 9.6.2 Sorting the Production Rules.- 9.6.3 Restricting the Search.- 9.6.4 Choosing Weights.- 9.7 Worked Example.- 9.8 Other Possibilities.- 9.9 Summary.- 10. Assessing Conjectures.- 10.1 Generic Measures for Conjectures.- 10.1.1 Type of Conjecture.- 10.1.2 Surprisingness.- 10.1.3 Other Generic Measures.- 10.2 Additional Measures for Theorems.- 10.2.1 Difficulty of Proof.- 10.2.2 Generality of Theorems.- 10.3 Additional Measures for Non-theorems.- 10.4 Setting Weights for Conjecture Measures.- 10.5 Assessing Concepts Using Conjectures.- 10.5.1 Independence of Measures for Conjectures.- 10.5.2 Identifying Concepts Discussed in Conjectures.- 10.5.3 Measures for Concepts.- 10.6 Worked Example.- 10.7 Summary.- 11. An Evaluation of HR’s Theories.- 11.1 Analysis of Two Theories.- 11.1.1 A Theory of Numbers.- 11.1.2 A Theory of Groups.- 11.2 Desirable Qualities of Theories — Concepts.- 11.2.1 Average Applicability of Concepts.- 11.2.2 Average Comprehensibility of Concepts.- 11.2.3 Number of Categorisations.- 11.2.4 Number of Concepts.- 11.3 Desirable Qualities of Theories — Conjectures.- 11.3.1 Difficulty and Surprisingness of Conjectures.- 11.3.2 Proportion of Theorems and Open Conjectures.- 11.4 Using the Heuristic Search.- 11.4.1 Robustness of the Heuristic Measures.- 11.4.2 Differences Between Domains.- 11.4.3 Pruning Using the Heuristic Measures.- 11.5 Classically Interesting Results.- 11.5.1 Graph Theory.- 11.5.2 Group Theory.- 11.5.3 Number Theory.- 11.6 Conclusions.- 12. The Application of HR to Discovery Tasks.- 12.1 A Classification Problem.- 12.2 Exploration of an Algebraic System.- 12.3 Invention of Integer Sequences.- 12.3.1 Additions to the Encyclopedia.- 12.3.2 Refactorable Numbers.- 12.3.3 Sequence A046951.- 12.4 Discovery Task Failures.- 12.5 Valdés-Pérez’s Machine Discovery Criteria.- 12.5.1 Novelty.- 12.5.2 Interestingness.- 12.5.3 Plausibility.- 12.5.4 Intelligibility.- 12.6 Conclusions.- 13. Related Work.- 13.1 A Comparison of HR and the AM Program.- 13.1.1 How AM Formed Theories.- 13.1.2 Misconceptions about AM.- 13.1.3 Programs Based on AM.- 13.1.4 A Qualitative Comparison of AM and HR.- 13.1.5 A Quantitative Comparison of AM and HR.- 13.1.6 Summary: The AM Program.- 13.2 A Comparison of HR and the GT Program.- 13.2.1 How GT Formed Theories.- 13.2.2 The SCOT Program.- 13.2.3 A Qualitative Comparison of GT and HR.- 13.2.4 A Quantitative Comparison of GT and HR.- 13.3 A Comparison of HR and the IL Program.- 13.3.1 How IL Worked.- 13.3.2 A Qualitative Comparison of IL and HR.- 13.4 A Comparison of HR and Bagai et al’s Program.- 13.4.1 How Bagai et al’s Program Worked.- 13.4.2 A Qualitative Comparison of HR and Bagai et al’s Program.- 13.5 A Comparison of HR and the Graffiti Program.- 13.5.1 How Graffiti Works.- 13.5.2 A Qualitative Comparison of Graffiti and HR.- 13.6 A Comparison of HR and the Progol Program.- 13.7 Summary.- 14. Further Work.- 14.1 Additional Theory Formation Abilities.- 14.1.1 Additional Production Rules.- 14.1.2 Improved Presentational Aspects.- 14.1.3 Further Possibilities for Making and Settling Conjectures.- 14.2 The Application of Theory Formation.- 14.2.1 Automated Conjecture Making in Mathematics.- 14.2.2 Constraint Satisfaction Problems.- 14.2.3 Machine Learning.- 14.2.4 Automated Theorem Proving.- 14.2.5 Application to Other Scientific Domains.- 14.3 Theoretical Explorations.- 14.3.1 Meta-theory Formation.- 14.3.2 Cross Domain Theory Formation.- 14.3.3 Agent Based Cooperative Theory Formation.- 14.4 Summary.- 15. Conclusions.- 15.1 Have We Achieved Our Aims?.- 15.2 Contributions.- 15.2.1 Functionality.- 15.2.2 Simplicity of Architecture.- 15.2.3 Cycle of Mathematical Activity.- 15.2.4 Generality of Methods.- 15.2.5 Mathematical Discovery.- 15.2.6 Evaluation Techniques.- 15.3 Automated Theory Formation in Pure Maths.- Appendix A. User Manual for HR1.11.- Appendix B. Example Sessions.- Appendix C. Number Theory Results.