The MATHsAiD Project

Project Description

The long-term goal of the MATHsAiD (Mechanically Ascertaining Theorems from Hypotheses, Axioms and Definitions) project consists of emulating a large portion of the human mathematical discovery process. The tasks involved in this process include the discovery/invention of definitions, axioms, concepts, theorems, problems and algorithms, plus the ability to perform verifiably correct computations. Many of these tasks were outlined by Prof. Buchberger during the Special Semester on Groebner Bases and Related Methods 2006.

The primary aim of the MATHsAiD project thus far has been to focus on theorem-discovery; to design and build a tool to automatically discover, prove and identify theorems (lemmas, corollaries, etc.) from a given set of axioms and definitions which are supplied by the user. No other input is required. This tool would, for instance, allow a mathematician to try several versions of a particular definition, and in a relatively small amount of time, be able to see some of the consequences, in terms of the resulting theorems, of each version. Moreover, the automatically discovered theorems could perhaps help the users to discover and prove further theorems for themselves. This system could also easily be used by educators (to generate exercise sets, for instance) and by students as well. In a similar fashion, this tool might also prove useful in enabling automated theorem provers to dispatch many of the more difficult proof obligations arising in software verification, by automatically generating lemmas which are needed by the prover, in order to finish these proofs.

Given a set of axioms and definitions for some particular theory, MATHsAiD analyses the information supplied, and based on this analysis, generates a sequence of sets of hypotheses. This sequence is designed to discover the more “routine” theorems in this theory; i.e., results that one might expect to see in a mathematics textbook. For example, in set theory, given the usual definitions of union and intersection, MATHsAiD discovers, among other things, that these operations are commutative, associative, and each is distributive over the other. For each set of hypotheses in the aforementioned sequence, MATHsAiD uses a combination of “generating” and “trivial” proof plans to discover all the more-or-less interesting results it can, subject to numerous constraints. In particular, the “generating” proof plans serve to derive (generate and prove) various conclusions c from the given hypotheses, whereas the “trivial” proof plans act as a constraint, by allowing the assertion of a newly-derived c only if it fails to be proven by any of the “trivial” proof plans. Once the system is no longer able to assert any additional conclusions, either because the combination of “generating” and “trivial” proof plans do not allow such, or because the time limit has expired, the generated conclusions are then passed to a final filtering stage, in which the less interesting ones are weeded out, leaving (hopefully) only the sorts of results that the user desires to see.

Progress thus far

In the early stages of this work, a prototype version of MATHsAiD was applied to domains such as set theory, group theory, the natural numbers, etc., albeit using only first-order terms.  (See the axioms provided to, and the Theorems discovered by MATHsAiD during those early stages, here). More recently, we enabled an altogether new implementation of MATHsAiD (2.0) to deal with higher-order objects. MATHsAiD now allows the user to introduce concepts such as, “the set of all x such that P(x)”, where P(x) is an open sentence. We have also had some success in automating the discovery of theorems which are typically proved by mathematical induction (see our paper Automated discovery of inductive theorems).

During the past few years we developed alternative methods for discovering new theorems; in particular we introduced “Theorem-producing rules” (TPRs) and “sketch-plans” (a slight variation of proof-plans). Preliminary results indicate that these new methods are more efficient (than our previous methods) at discovering quality theorems, primarily because they prohibit the generation of most lower-quality results in the first place. A research paper explaining these methods is currently in preparation.

We have also developed certain inter-theory reasoning capabilities within MATHsAiD, designed to identify interesting connections between theories -- even if at first glance those theories appear to be entirely unrelated. For example, MATHsAiD automatically discovered, once the theory of semi-rings and the theory of topologies were both in place, that a topology can be viewed as a semi-ring in two distinct ways. Note that such inter-theory results are simply beyond the capability of most first-order resolution theorem provers (for example).

We use the MathJax display engine to display our results. MathJax is sponsored in part by the American Mathematical Society; it provides excellent-quality, scalable mathematical typesetting in most browsers. On a personal note, we have found it to be quite useful/advantageous in our own work with the MATHsAiD system.

Results The theories thus far explored in MATHsAiD.

Collaborations

MATHsAiD has been included as a part of the ATLAS prototype system, which is designed for automated reasoning in large structured theories. This work was funded by EPSRC Visiting Researcher Grant EP/E005322/1, during the summer of 2006. MATHsAiD has also been integrated into the interactive mathematical authoring system PLATO. We have also begun collaborations with the ACL2 group in Austin, Texas.

People

Publications

Funding

The MATHsAiD project has been funded by EPSRC Grant EP/F033559/1, for the period 2007-2011, and by EPSRC MathFIT Grant GR/S31099, during 2003-2006.