How TheoryMine Worked

WHAT IS A THEORY?

From school mathematics you will recall various kinds of numbers: whole numbers, fractions, decimals, etc. You may also have met sets or vectors. These are all examples of mathematical objects. The first thing that TheoryMine does is create new kinds of mathematical object and it can generate an unlimited number of these. In school mathematics you apply functions to numbers, such as addition and subtraction. The second thing that TheoryMine does is create new kinds of functions on these new mathematical objects. TheoryMine can also generate an unlimited number of functions. A Theory is composed of one or more mathematical objects plus some functions on such mathematical objects.

WHAT IS A THEOREM?

A theorem is a mathematical formula for which we have a proof. Both theorems and proofs are within a theory which consists of a set of axioms. A proof is a sequence of formulae, starting with some axioms and ending with the theorem. Each non-axiom formula in this sequence follows from the previous formulae in the sequence. All the axioms in TheoryMine theories are recursive definitions.

WHAT IS A RECURSIVE DEFINITION?

Recursion is a mathematical technique that is much used in computer programs. In a recursive definition, the value of a recursive function is defined in terms of values of the same function applied to smaller inputs. This sounds circular, but because the function's inputs get smaller and smaller the computation eventually stops. TheoryMine also uses recursion to define brand new types of input and output for each theory. These are called recursive objects.

WHAT KIND OF THEOREM DOES THEORYMINE DISCOVER?

TheoryMine proves properties of functions. For instance, when it comes to addition, it does not matter in which order the numbers are added: 2+3 is equal to 3+2, whereas when it comes to subtraction it does: 2-3 is not equal to 3-2. TheoryMine might discover that some of its functions are like addition; giving equal answers whatever the order of the objects to which they are applied. Some functions are inverses of each other, e.g. addition and subtraction: adding a number and then subtracting it, brings you back to where you started. TheoryMine might also discover that some of its new functions are also inverses. The theorems discovered by TheoryMine typically take this simple form.

HOW CAN I BE SURE THAT THE PROOF OF MY THEOREM IS CORRECT?

The computer programs behind TheoryMine are large and complex and so, like all large complex programs, almost certainly contain bugs However, most of the program merely chooses theories and theorems to prove, and directs their proof. The construction of the proof is handled by a small, well inspected and highly trusted kernel program that only combines axioms and previously proved theorems. It is therefore vanishingly unlikely that any proof it constructs would be faulty.

HOW IS IT POSSIBLE TO GENERATE THEOREMS?

TheoryMine is based on decades of world-class research into automated reasoning and artificial intelligence at the Universities of Edinburgh, Cambridge and Munich. It uses the grammars of theories and theorems to generate candidates, filters out the obviously false and uninteresting ones, and then uses automated reasoning to see which of the remainder it can prove.

HOW CAN I BE SURE MY THEOREM IS ORIGINAL?

The TheoryMine program constructs brand new mathematical theories, that no-one has previously developed by using brand new recursive functions and recursive objects. By definition, all theorems of these new theories are themselves brand new.

HOW CAN I BE SURE THAT MY THEOREM IS NOT TRIVIALLY TRUE?

There are two senses in which your theorem is not trivially true. Firstly, note that some mathematical theories are inconsistent i.e. the axioms contradict each other. In such theories all formulae are theorems, which is clearly undesirable. However, it is a well-established mathematical result that theories consisting only of recursive definitions, as TheoryMine's theories are, are inherently consistent. So you can be sure that your theorem is not trivial in this sense. The second sense in which these theorems are not trivially true is that they cannot be directly derived by a simple calculation. In particular, they are not true by simple rewriting from other known theorems, as described in more detail in the answer to the question: IS MY THEOREM INTERESTING?.

IS MY THEOREM INTERESTING?

TheoryMine applies a series of filters to remove uninteresting theorems before it generates them. On the other hand, don't expect your theorem to earn you the Fields Medal! (the Nobel Prize of Mathematics). In particular, we use the notion of interesting initially developed in Conjecture Synthesis for Inductive Theories (Journal of Automated Reasoning) which was then further developed in Scheme-Based Synthesis of Inductive Theories (LNCS, Volume 6437). Technically, this ensures that standard orderings, using known theorems as rewrites, cannot prove the new theorem: that there is no direct symbolic calculational proof of the new theorem.

BY WHAT AUTHORITY CAN I ASSIGN A NAME TO MY THEOREM?

It is a long-standing tradition in mathematics that the author of a new theorem has the authority to name it. TheoryMine assigns that authority to you.

WHY DO YOU CLAIM THAT THEOREMS LAST FOR EVER?

A theorem, once proved, stays proved for ever. The reasoning in the proof is deductive, so contains no element of probability or uncertainty. Theorems are abstract objects that are not subject to wear and tear. Even diamonds will be destroyed in the heat death of the universe; theorems won't be.