Automated Theory Formation in Pure Mathematics

1. Front Matter

   Pages iii-xvi

   PDF

2. Introduction

   • Simon Colton

   Pages 1-8

3. Literature Survey

   • Simon Colton

   Pages 9-28

4. Mathematical Theories

   • Simon Colton

   Pages 29-43

5. Design Considerations

   • Simon Colton

   Pages 45-58

6. Background Knowledge

   • Simon Colton

   Pages 59-67

7. Inventing Concepts

   • Simon Colton

   Pages 69-100

8. Making Conjectures

   • Simon Colton

   Pages 101-120

9. Settling Conjectures

   • Simon Colton

   Pages 121-140

10. Assessing Concepts

    • Simon Colton

    Pages 141-163

11. Assessing Conjectures

    • Simon Colton

    Pages 165-179

12. An Evaluation of HR’s Theories

    • Simon Colton

    Pages 181-223

13. The Application of HR to Discovery Tasks

    • Simon Colton

    Pages 225-245

14. Related Work

    • Simon Colton

    Pages 247-279

15. Further Work

    • Simon Colton

    Pages 281-293

16. Conclusions

    • Simon Colton

    Pages 295-301

17. Back Matter

    Pages 303-380

    PDF

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.

• Addition
• Automated Theory
• Computational Creativity
• Computer
• Equivalence
• Machine Learning
• Pure Mathematics
• artificial intelligence
• calculus
• classification
• database
• intelligence
• number theory
• proving

• University of Edinburgh, Edinburgh, UK

  Simon Colton

Policies and ethics