Current MATHsAiD Results

Unlike the original version of MATHsAiD (which was, after all, only ever intended to be a prototype), in which the logic was hard-coded, the current version of MATHsAiD allows the users to specify their logic of choice (within certain limits). For our logic, we have chosen a variation of Natural Deduction, including quantifiers. We also have a theory of equality, in which 'equals' is simply declared to be an equivalence relation, with an additional property regarding substitution. In certain theories we have included additional axioms regarding 'equals' (e.g., “extensionality”, in the theory of Classes).

Most of the remaining (non-inductive) theories represented in this work are based primarily on the excellent and widely used text, Algebra, by Thomas W. Hungerford, published in Springer's Graduate Texts in Mathematics series. In particular, we begin with the theory of classes, where sets are just special kinds of classes. We of course will, from time to time, vary slightly from Hungerford (for example, we introduce relations prior to functions, rather than the other way round). While the results posted here admittedly represent only a very small portion of the work contained in the text, it is perhaps sufficient to suggest that our system can indeed deal adequately with higher-order objects -- an important aspect of any automated mathematical reasoning system.

Another important aspect is the ability to reason in inductive theories. While inductive theories have not been the main focus of this particular project, nevertheless, as previously mentioned, MATHsAiD has likewise demonstrated an ability to deal successfully with such theories.


This page contains links to the results thus far produced by MATHsAiD, in the aforementioned theories. For each theory, one can find the Axioms/Definitions/Notation provided to MATHsAiD and the Theorems/Facts/Examples discovered and proven by MATHsAiD. Note that under normal circumstances, MATHsAiD is programmed to try to prove the converse of each Theorem it finds -- without regard to whether the converse itself would pass through the theorem filtering process. Also note that the system's discoveries are now separated into three categories: Theorems, Facts and Examples. (These distinctions are probably not terribly important -- but might be viewed by some users as a feature). 'Facts' consist primarily (but not exclusively) of the sorts of results which are sometimes referred to as type information, plus results which in effect serve to 'unpack definitions'. Such results are usually not specially designated in mathematics textbooks as Theorems, Lemmas, Corollaries, etc., but are often relegated to the text, or perhaps to exercises. As for 'Examples', these refer primarily to the results produced by the aforementioned inter-theory reasoning.

Note that the user has the option of instructing the system to provide alternate (human-readable) representation for any given term. In a sense, the system is capable of translating from its own notation into a notation more suited to the human eye. We have indeed taken advantage of this capability on many occasions. For example, in order to fully specify a particular ring, one ought to provide names for the ground set, plus the addition and multiplication operations, plus the additive identity. In the introductory definition of 'ring', this is precisely what we do. However, for each occurrence of 'ring' following its original introduction, we prefer not to have to look at the 'extra clutter', but choose instead to follow the usual convention of simply referring to the ring by the name of its ground set -- this is all we want to see. Be aware, however, that the system only operates on the 'full' notation -- the 'abbreviated' notation is simply for the sake of the human eye.

When it comes to the html files listed below, for those terms for which we want alternate representation/notation, we generally follow the pattern described above; that is, the first time the term appears, the 'full' notation appears; thereafter, an 'abbreviated' version appears. That said, in the system itself, both the 'full' and the 'abbreviated' versions appear (see the screen shot).

Pressing ahead

We point out that, at present, we have left several of the theories listed below only partially completed (indeed some of our theories consist of only one or two axioms/definitions, plus whatever results could be proven from these -- little more than 'bare-bones'). Moreover, within some theories we have, for the time being, included some 'provable' axioms -- that is to say, some of our 'axioms' could in fact have been proven, provided there had been sufficient theory development. Furthermore, some of the 'manual mode' results (see below) could have been found automatically; again, provided there had been sufficient theory development.

The main reason for all this is that we wanted to press ahead, to get certain results that could be described as fairly 'advanced' (for example, the aforementioned Zariski space result) -- without spending the necessary time required to fully 'flesh-out' all the prerequisite theories. One consequence of this approach is that we have indeed demonstrated MATHsAiD's ability to produce some 'advanced' results, despite the relative lack of fully-developed underlying theories. Of course, one is always free to return to any theory, at any time, in order to add or remove data as one sees fit (and we fully intend to someday replace all the 'provable' axioms with theorems/facts).

Manual Mode

While we have admittedly left several theories rather sparse, certain theories have been supplemented with additional Theorems/Facts/Examples, by using the 'Manual' mode of MATHsAiD; i.e., the hypotheses were provided by hand, along with either a conjecture to be proved or a 'term of interest' to be explored (that is, a term about which the user would like the system to discover whatever interesting results it might find). In particular, we have added (in this fashion) into some theories a number of Facts which were necessary in order for the system to prove certain desired results in either that or some subsequent theory. In addition, we also added a few Theorems (see the theories of Logic and Naturals, for example) which arguably most mathematicians would expect to see, but which the system failed to find on its own (in 'Automatic' mode). Note that all results obtained in 'Manual' mode have in fact been proven 'automatically' by the system -- it is simply that the conjecture to be proven ('term of interest' to be explored) was input manually by the user.


One further comment -- there are admittedly some Theorems/Facts/Examples which are of rather less quality than one might wish to see in a list of 'interesting/useful' results (though we suggest that, amongst the Theorems, there are not so terribly many, considering that they were found and identified automatically by a machine). In particular, we have found it rather expedient to produce/record Facts which, in effect, unpack definitions -- especially definitions regarding algebraic structures (e.g., a ring is an Abelian group, which is a group, which is a monoid, etc.). Such Facts are, for the most part, quite uninteresting to humans; however, their presence within the system considerably reduces the amount of time needed to explore these structures.

In any event, it is quite easy to remove (with the push of a button) any undesirable results. Nevertheless, we have chosen, for the time being, to leave all the lower-quality results in the database, not only for reasons of expediency, but, perhaps more importantly, so that the scientific community might examine the unabridged results.

Non-Inductive Theories

  • BinaryOperations
  • Classes
  • Equality
  • Functions
  • Graphs
  • Groups
  • Logic
  • Modules
  • Monoids
  • MVarieties
  • Orderings
  • Relations
  • Rings
  • RVarieties
  • ScalarMultiplic
  • Semigroups
  • Semimodules
  • Semirings
  • Sets
  • Topologies
  • ZariskiSpaces
  • ZariskiTopology
  • Inductive Theories

  • Lists
  • Naturals

  • Last Updated on 04/07/2012