You can name your very own mathematical theorem, newly generated by one of the world's most advanced computerised theorem provers (a kind of robot mathematician), and you can immortalise your loved ones, teachers, friends and even yourself and your favourite pets.

I would be afraid that I would not understand my own theorem (see here for an example).

I will stick with Tabarrok's Wager (original paper here).

Hat tip: Boing Boing.

For the record, here's a translation of the example into natural language. Judging whether the theorem is genuinely interesting is left as an exercise to the reader.

Let T be a set defined as follows. An element of T is either:

…… (base case) an ordered pair of booleans (truth values), or;

…… (inductive case) the successor of any element of T.

If an element of T is an ordered pair of booleans, then it is not the successor of any element of T. Moreover, these two cases are exhaustive.

If any two elements of T are equal (not equal), then their successors are equal (not equal), respectively.

Let (

a`mw`b) be an operation defined as follows:…… (base case) If

ais an ordered pair of booleans, the result isb.…… (inductive step) If

ais the successor of an element of T (call ita'), the result is the successor of (a'`mw`b).Quentin's Theorem: mw is associative.

Nicely done, anon at 10:07. Beat me to it by 12 minutes.

By the way, the notation by which you infixed mw, is that just a Haskell thing or more general?

The non-machine proof of Quentin's theorem is also fairly trivial.

By definition, every element of T is of the form C2(C2…(C1(b1,b2)) where C2 is repeated n times and b1 and b2 are arbitrary boolean variables.

By applying the definition to mw(C2^n(C1(b1,b2)),C2^n'(C1(b1',b2'))), we see that it equals C2^(n+n')(b1',b2'). In other words, mw is just over-complicated representation of addition and is associative because addition is.

BTW, many dynamic programming algorithms (think optimality principle) are frequently presented in similar obscure terms, so this is by no means a rare disease.

I was actually thinking we will get some theorems in the sense of verified code or some such. The ml/haskell notation threw me off a bit.

I would be afraid that my theorem had already been proved in the 40's in some otherwise forgotten dissertation. Then some dissertation reading program in the year 2034 will discover it and strip me of my theorem.

(I am also afraid that a similar program will read my own dissertation, decide that it is crap, and start agitating to get my Ph.D. revoked)

Those aren't real maths, I swear.

Anyway, thanks for the translation Anon. Sterling stuff.

@Silas don't worry too much about 'succession', you can make it up as you go along. You can expand the explanation as

"for every element A of T there exists some element S(A) called the successor of A, such that …".

So in the case of the integers this means "for for every number N there is a number denoted N+1".

Anyway, can anyone confirm if Corporate Serf is right? I'm not great shakes on number theory, but I mostly agree with him. However, it seems that all for elements of the "base case" plays the role of zero. I doubt they are all be additive identities, indeed I bet you can't define addition. If so, then T is definitely not the natural numbers, and Quentin's theorem is a true generalisation of the associativity of addition.

Moreover, it probably works beyond this dirty, two-bit rascal, base case.

"T is definitely not the natural numbers, and Quentin's theorem is a true generalisation of the associativity of addition."

It's a true generalization, but (IMHO) not a very interesting one. Yes, the set T is isomorphic [ignoring corner cases] to âŸ¨bool Ã— bool Ã— â„•âŸ©, where

âŸ¨

a,b,nâŸ© `mw_iso` âŸ¨a',b',n'âŸ© = âŸ¨a',b',n+n'âŸ©The function mw_iso can be split component-wise; associativity of addition is known, and the bool components are also associative since they are right-zero semigroups. And no, there isn't any identity element: mw is a semigroup, but it's not a monoid.

My view is that automatically formulating conjectures which are both novel and reasonably interesting is a very hard task; doing it reliably is all but impossible. Things would improve if we had a comprehensive archive of formalized mathematics, but even then, robot mathematicians will mostly be tasked with "refactoring" theories (finding generalizations, searching for redundancies and the like) and proving existing theorems.

Comments on this entry are closed.