Project: Funded Project › Research

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

Total award | £517,261.00 |
---|---|

Funding organisation | EPSRC |

Funder project reference | EP/F033559/1 |

Period | 1/11/07 → 31/12/11 |

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

Synopsis: The aim of the project was to build a tool, MATHsAiD 2.0, that would be a useful aid to the working mathematician, by conjecturing and proving many of the interesting theorems of a given mathematical theory (from user-provided axioms), whilst limiting the number of non-interesting theorems generated.

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.

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.