AUTOMATED DISCOVERY OF MATHEMATICS

Synopsis: The aim of the project was to build a tool, MATHsAiD 1.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: Given the axioms of a mathematical theory, conjecture and prove all and only the interesting theorems of that theory up to some resource limits.
Evaluation: We have successfully evaluated the hypothesis on a diverse and representative set of axiomatic theories that includes some inductive theories. Our experimental methodology consisted of a precision/recall comparison of MATHsAiD 1.0's selection of interesting theorems with that of the authors of prominent textbooks writing about the same axiomatic theories. We have shown that the difference between MATHsAiD 1.0's selection and the selections of these authors is not significantly different from the differences between each of these authors and the remaining selections. That is, MATHsAiD 1.0's variation is comparable with that of a typical, expert human's.