Automated Theorem Discovery

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.