Edinburgh Research Explorer

Automated Theorem Discovery

Project: Funded ProjectResearch

Total award£517,261.00
Funding organisationEPSRC
Funder project referenceEP/F033559/1
Period1/11/0731/12/11
Project websitehttp://dream.inf.ed.ac.uk/projects/mathsaid/

Key findings

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.