^{TM}
Personalized mathematical theorems 
... you could be next!

The following is an example of a certificate generated by TheoryMine. An explanation of a formula can be obtained by clicking on it.
This particular theorem was created in honour of Quentin Cooper, who interviewed us for the BBC Radio 4 science magazine programme Material World on 15th April 2010. The certificate above is different from the one originally presented to Quentin. We have updated it into the format of the certificates we currently issue to customers. In particular, we have now standardised the way we name the various mathematical expressions.
Following the name of the theorem, Quentin's Theorem,the certificate contains, in turn: the definition of a new kind of mathematical object, T; the definition of a new mathematical function, f_{α}; and the statement of the theorem.
One way to envisage T is as four copies of the nonnegative whole numbers 0, 1, 2, 3, ..., each copy in a different colour, say red, blue, green and yellow: 0, 1, 2, 3, ..., 0, 1, 2, 3, ..., etc. So each member of T has both a numerical value and a colour. f_{α} is then a kind of addition on these numbers. Its inputs are two coloured numbers and its output is a third coloured number, whose numerical value is the sum of those of the inputs and whose colour is that of the second input.
Note that, unlike regular addition, f_{α} is not commutative, that is its output depends on the order of its inputs. For instance, f_{α}(1, 2)= 3 but f_{α}(2, 1)=3. Notice that the numerical values of the outputs are the same, but the colours are different, as they depend on the colour of the second input.
However, if we add three coloured numbers together, then the order of the first two is immaterial. This is because the colour of the output will be that of the third input, so will not depend on the colours of the first two inputs. For instance, f_{α}(1, f_{α}(2,3)) = f_{α}(2, f_{α}(1,3)) since both sides equal 6. The generalisation of this equality is Quentin's Theorem, i.e., it is a restricted variant of commutativity.
We now give a more technical explanation of the certificate. The technical terms used in this explanation are also defined in the glossary at the end.
Both T and f_{α} are defined byrecursion. This is a form of definition in which the body of the definition contains the thing being defined. This sounds circular, but it need not be. Consider, the following recursive definition of the, so called, natural numbers, i.e., the nonnegative whole numbers 0, 1, 2, 3, ....
where s is called the successor function. This definitiongenerates a representation of the natural numbers of the form 0, s(0),s(s(0)), s(s(s(0))), ..., where each application of s increases the number by 1. This representation is due to the mathematician Giuseppe Peano (18581932). The recursive definition consists of two cases: a base case 0 and a step case s(N). Any particular natural number corresponds to one of these cases. Note that the step case contains N, which is the thing being defined. Think of this, not as a circle, but as a spiral. 0 is at the centre of the spiral; each application of s winds the spiral out by a complete circuit. 0 and s are called constructor functions, because they are used to construct new types of mathematical objects, such as our fourcoloured numbers. Note that constructor functions are deliberately not defined. They are taken as primitive mathematical objects and are used in the definitions of other mathematical objects and defined functions, such as +. Definitions have to stop unfolding at some point, and that point is with the constructor functions.
The boolean truth values, true and false, can be defined by a degenerate form of recursion, in which there are two base cases and no step cases: B = true  false.
We will use B and N as the basis for defining new sets of recursively defined mathematical objects, such as T in our example certificate above.
The function + can also be defined recursively. It takes two members of N as inputs and returns one as output. It also has a base case and a step case.
The type line says that + takes two natural numbers as inputs and outputs one natural number. The base case and step case lines constitute the recursive definition of +. The recursion is on x, the first input of +. Note that, in the step case, the body of the definition also contains +, the function being defined. This is also not a circular definition, but a spiral one. This time the recursion spirals inwards. Starting with some particular value of x, say s(s(o)), the step case is applied to rewrite s(s(0))+y first to s(s(0)+y) and then to s(s(0+y)). Now the base case of the definition can be used to rewrite this as s(s(y)) and the calculation is finished. Notice how the step case is organised so that + is applied to a smaller occurrence of x in the body of the definition than in the head. N has been defined to be well founded, which means that a sequence of its members cannot keepgetting smaller forever: sooner or later it will reach 0. This means that any calculation carried out using + will eventually stop. We can only apply the step case a finite number of times. Eventually, only the base case will be applicable and, after the base case, nothing will be applicable. To contrast functions such as + with the constructor functions, such as 0 and s, + is called a defined function.
Our certificate introduces a new type of mathematical object called T, our fourcoloured numbers. T is defined recursively as:
where C_{a} and C_{b} are new constructor functions. C_{a} is a base constructor, since it does not have T among its inputs. It is analogous to the 0 constructor function of N, except that it has two inputs. These inputs are both members of B, i.e., they are one of two truth values: true and false. There are, therefore, four ways to instantiate C_{a}: C_{a}(true,true), C_{a}(true,false), C_{a}(false,true) and C_{a}(false,false), i.e., there are four versions of 0. Above we envisaged these four versions of 0 as four differently coloured 0s, e.g., C_{a}(true,true) could be envisaged as 0 and C_{a}(true,false) as 0.
C_{b} is a step constructor, since it does have T among its inputs. It is analogous to the s constructor function of N. The main difference to s is that C_{b} can be applied to four different kinds of base constructor. We can envisage these C_{b} applications as colour preserving. For instance, since C_{b}(C_{b}(C_{a}(true,true))) has a 0 at its heart, we can envisage it as 2.
Note that, just as with 0, s, true and false, the new constructor functions, C_{a} and C_{b} are undefined primitives.
Compare this definition to that of + above. It's essentially the same. f_{α} is just a version of addition.
To see why each output of f_{α} has the same colour as its second input, consider first the base case. The first input of f_{α} is one of the coloured 0s, C_{a}(x,y), but regardless of its colour, the output is its second input, z, so it necessarily has the same colour as this second input.
Now consider the step case of the definition of f_{α}. Assume that we have already inferred that the output of f_{α}(x,y) has the same colour as its second input y. Since C_{b} is colour preserving, then f_{α}(C_{b}(x),y) also has the same colour as y, which is its second input. In this way, starting from the situation when f_{α} has first input C_{a}(x,y), we can incrementally spiral out showing that the argument holds for each application of C_{b} and, therefore, for every member of T. This is called an inductive proof. It is the same kind of reasoning that TheoryMine uses to prove all the theorems that it generates.
.On the certificate, Quentin's Theorem is said to be proved by "induction on y". What does this mean?
Induction is closely related to recursion. Theorems composed of recursively defined functions applied to recursively defined objects, such as Quentin's theorem, are usually proved by induction. Firstly, an induction variable is chosen. In this case it is y  although, as Quentin's Theorem is symmetric with respect to x and y, it could equally well have been x. The induction variable will range over some recursively defined mathematical object. In our case, y ranges over objects of type T.
Just like a recursive definition, an inductive proof is divided into base and step cases.
and then have to prove:
At first sight, inductive proofs look circular. During the proof of the step case, we assume the theorem already holds. But, once again, the inductive proof is really spiral. We start by proving that the theorem holds for the centre of the spiral (the base case), then the step case can be used to prove that it holds for one circuit of the spiral, then for two circuits, then three, and so on for any number of circuits.
The base case can be proved by two applications of the base case of the recursive definition of f_{α}, namely f_{α}(C_{a}(u,v),w) = w , where I have renamed the variables to avoid confusion with those in the theorem. These can be used to rewrite the base case in two stages, as follows:
At this point, the equation is between two identical expressions, so the base case is proved.
In the step case, the induction conclusion can be proved by:
The induction conclusion is rewritten in three stages, as follows:
The induction hypothesis can now be used to rewrite the left hand side to:
At which point, the equation is again between two identical expressions, so the step case is proved. The lemma was previously proved by TheoryMine and is called The Richard Scott Russell Theorem . Its proof is also by induction and is left as an exercise for the reader.
The fourcoloured numbers described above are just one among infinitely many possible new mathematical objects. Different kinds of objects are generated by the choice of base and step constructors and by the inputs that we give them. For instance, suppose we had chosen to give C_{a} only one boolean input.
Then there would only be two 0s, so the numbers would have only two colours.
Alternatively, we could have had two base case constructors.
Now there would be eight 0s, so the numbers would have eight colours.
Or we could have given the base constructor a natural number as its input.
Now there would be an infinite number of 0s and so infinitely many colours of numbers.
It gets more interesting if we give the step constructor additional arguments.
Now there are infinitely many different kinds of successor function. Another way to think of this is as defining a sequence of natural numbers, i.e., the numbers associated with each of the successor functions used in a number. So, C_{b}(C_{b}(C_{b}(C_{a}(true,true),1),3),2) would be the sequence 1,3,2, for instance.
Nor do we have to stick to B and N as inputs to these constructor functions. Having defined T, for instance, we could use it as an input to a constructor function for some new objects T',
which would allow us to have sequences of differently coloured numbers: 1, 3, 2.
We have collected together the definitions of some of the technical terms used in this explanation. These terms have alternative names in mathematics and computer science. We also give some of their synonyms.