Project: Research

- Bundy, Alan (Principal Investigator)
- Colton, Simon (Co-Investigator (External))
- Smith, Patrick (Co-Investigator (External))

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

Effective start/end date | 1/08/03 → 31/08/06 |

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

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.

## Automated Discovery of Inductive Theorems

Research output: Contribution to journal › Article

## Ascertaining Mathematical Theorems

Research output: Contribution to journal › Article

## MATHsAiD: A Mathematical Theorem Discovery Tool

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

## A Common Type of Rigorous Proof that Resists Hilbert’s Programme

Research output: Chapter in Book/Report/Conference proceeding › Chapter (peer-reviewed)