Automated Theorem Discovery

Lead Research Organisation: University of Edinburgh
Department Name: Sch of Informatics

Abstract

This project represents the second stage of a multi-stage project, the long-term goal of which is to emulate a large portion of the human mathematical discovery process. The focus of this particular stage is on fully developing and deploying an Automated Theorem Discovery (ATD) system. By ATD system we mean a system that automatically generates, proves and identifies a significant number of mathematical results which mathematicians are likely to recognize as Theorems, Lemmas, Corollaries, etc. (as opposed to the sorts of results which, true though they might be, would probably not be deemed worthy of recording).Generations of mathematicians have appreciated the benefits of building a mathematical knowledge base bit by bit, Theorem by Theorem, in that previously discovered results often prove quite useful -- perhaps even necessary -- in the discovery and the proof of subsequent results. Moreover, since the advent of the modern computer, it has become increasingly apparent that automated reasoning (AR) systems can likewise benefit from a similar incremental build-up of Theorems. This is especially true for certain formal verification problems, in which state-of-the-art automated theorem provers can dispatch some -- but not all -- of the generated proof obligations. The remaining proofs can only be achieved once certain Lemmas have been discovered; at present, this discovery must be done by hand.We therefore anticipate that an effective and practical ATD system would be very useful, not only to mathematicians, but to computer scientists as well -- particularly those who work in formal verification. Indeed, in the latter case, we have supporting evidence (in the form of letters of support) that the potential payoff for such a system is huge.

Publications

10 25 50
publication icon
Bundy A (2015) The Theory behind Theory Mine in IEEE Intelligent Systems

publication icon
Bundy A (2011) Automated theorem provers: a practical tool for the working mathematician? in Annals of Mathematics and Artificial Intelligence

publication icon
Bundy, A (2010) The Theory Behind TheoryMine in Automatheo. FLoC

publication icon
McCasland R (2017) MATHsAiD: Automated mathematical theory exploration in Applied Intelligence

publication icon
Montano-Rivas O (2012) Scheme-based theorem discovery and concept invention in Expert Systems with Applications

publication icon
Sorge V (2007) Automatic Construction and Verification of Isotopy Invariants in Journal of Automated Reasoning

 
Description 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.
Exploitation Route We continue to develop the MATHsAiD system using funding from our Platform Grant and in the personal time of the, now retired, RA, Roy McCasland. We will continue to promote its use as a practical tool to assist the working mathematician, increasing their productivity and accuracy.

MATHsAiD is specifically aimed at working mathematicians, but some of the techniques may find application elsewhere, e.g., in formal methods.
Sectors Digital/Communication/Information Technologies (including Software),Education,Other

URL http://dream.inf.ed.ac.uk/projects/mathsaid/
 
Description EPSRC
Amount £1,140,286 (GBP)
Funding ID EP/J001058/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Academic/University
Country United Kingdom
Start 08/2011 
End 07/2015