Conjecture making is a significant activity in mathematics, yet the question of producing mathematical conjectures by computer has only been addressed in isolated domains and with specialised techniques. We propose here to study and implement an important aspect of automatic conjecture making in mathematics: "Cross Domain Conjecture making": to determine procedures which, when implemented, will enable a program to make conjectures involving concepts from many different areas of mathematics.

We also propose to study and implement an important application of automatic conjecture making: "Theorem proving by Theory Formation": to determine and exploit the advantages of automatically proving theorems in an environment where new concepts can be introduced and explored, calculations can be made and relevant lemmas can be formed, proved and used. By addressing cross domain conjecture making, we hope to derive techniques which will one day lead to programs able to assist mathematicians by providing useful and intelligent conjectures about objects of interest. Proving a theorem often requires calculations, finding examples, inventing definitions and making conjectures. By integrating mathematical software to enable all of these activities, we hope to demonstrate the advantages of proving theorems in a theory forming environment.

The full proposal relating to this project is available HERE.

The of this project is available HERE.

The EPSRC IGR form for this project is available HERE.