Project: Research

- McCasland, Roy (Principal Investigator)
- Bundy, Alan (Co-investigator)

Status | Finished |
---|---|

Effective start/end date | 1/11/07 → 31/12/11 |

Links | http://dream.inf.ed.ac.uk/projects/mathsaid/ |

Hypothesis: MATHsAiD 2.0 can conjecture and prove interesting theorems in high-level theories, including theorems of current mathematical significance, without generating an unacceptable number of uninteresting theorems.

Evaluation: We have successfully evaluated the hypothesis by showing that MATHsAiD 2.0 is able to work in the theory of Zariski Spaces, which is a topic which the RA and Co-Investigator have worked on in their capacity as professional mathematicians. In particular, MATHsAiD 2.0 was able to conjecture and prove a key theorem from one of their papers. This key theorem was just one example of a theorem that relates two different theories, of which MATHsAiD 2.0 has proved several. It is unusual for automated theorem provers to prove theorems that relate multiple theories, but they are a common aspect of modern mathematics.

## Automated theorem provers: a practical tool for the working mathematician?

Research output: Contribution to journal › Article

## Scheme-based theorem discovery and concept invention

Research output: Contribution to journal › Article

## Automatic Construction and Verification of Isotopy Invariants

Research output: Contribution to journal › Article

## The Theory Behind TheoryMine

Research output: Contribution to journal › Article

## Scheme-Based Synthesis of Inductive Theories

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

## MATHsAiD: Automated Mathematical Theory Exploration

Research output: Contribution to journal › Article