Name a new math theorem after yourself or a loved one

TheoryMine runs a computerized mathematical theorem prover that turns out new mathematical theories all day long. For a mere $15, they'll name the theorem after you or someone you love: "Theorems are discovered by our robot mathematicians, we make every effort to ensure that the discovered theorems have never been published before, and we guarantee that every theorem we discover has not been previously recorded in our database of theorems. In the unlikely event that that there is a mathematics article publishing the theorem prior to our discovery, then we will give two additional new theorems to the owner of the old theorem." (via MeFi)

I write books. My latest is a YA science fiction novel called Homeland (it's the sequel to Little Brother). More books: Rapture of the Nerds (a novel, with Charlie Stross); With a Little Help (short stories); and The Great Big Beautiful Tomorrow (novella and nonfic). I speak all over the place and I tweet and tumble, too.

MORE: Science

More at Boing Boing

The technology that links taxonomy and Star Trek

Hackers prepare for first "national holiday" in their honor

SamSam

I took an automated theorem proving class when studying my master’s in AI at the University of Edinburgh — possibly the same class that the author of this site took, since it said that she developed it while at Edinburgh. Unlike her, though, I hated the course and didn’t understand half of it.

In principle it was kind of neat, though. Using a system that has a huge database of theorems — from the trivial, like Boolean logic and modus ponens to more complex published theorums — you give it something you want to solve, and it starts trying to work its way towards it. Often it throws up its hands and says “I got no idea what to do now,” and then the human looks at the various possible routes it can take and advises it on its next steps. Whether it’s a human solving the problem with a computer’s help or a computer solving it with the human’s help is hard to say.

Never-the-less, I wasn’t enough of a mathematician to enjoy the class, and skipped it more times than I probably should have…
Tensegrity

I’d name one Yatima.
Ushao

Strange coincidence that I just read this article last night.
http://science.slashdot.org/story/10/12/06/0416250/Medical-Researcher-Rediscovers-Integration
- SamSam
  
  That’s amazing. The guy’s article has 137 citations according to Google Scholar. Maybe the ADA Diabetes Care journal doesn’t employ any mathematicians on its peer-review board? A search for “Tai’s model” on Google finds a lot of face-palming.
CuttingOgres

I can think of a whole bunch of naughty names for theorems…
- Anonymous
  
  TheoryMine uses a list of known ‘naughty words’ to filter out offensively named theorems. Of course, no such list is complete, so some naughtily named theorems are bound to slip through. We have plans for buyers to opt into having their theorems publically displayed. There will then be a reporting button for anyone who finds CuttingOgres, or anyone else’s theorem names offensive, and we’ll take them down.
Anonymous

I’m gonna have so many theorems named after me.
endymion

Huh… Where do you guys find this stuff?

Fun idea. Two things cause the mathematician in me some distress:

1. I can’t find a single example on the website of a generated theorem. They claim that they also provide “a short explanation of the significance of each theorem, so you can see why it is interesting.” But I can’t find one example of a theorem and the explanation of why it’s interesting.

2. The FAQ has a good question: “HOW CAN I BE SURE THAT MY THEOREM IS NOT TRIVIALLY TRUE?” Their answer is the mathematical equivalent of political side-stepping: “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 theories are, are inherently consistent. So you can be sure that your theorem is not trivial in this sense.”

Great, dude, but that’s not the sense in which I was asking the question. (Just because your formal system can’t prove every statement doesn’t mean the ones it can prove are “NOT TRIVIALLY TRUE”.) Why even include the question if you’re going to give such a lame answer to it? :)
- Anonymous
  
  Well put…Theorems are pretty hard to come by, but still they probably could spit out someone once in awhile. Just cannot believe that at $15 a pop, you will make more than $15K ever! Oh well, what do I know…Who ever thought that people would like Twitter either?
Lobster

I’ll name one after my mother. Preferably one that I don’t even begin to understand, gives me a headache if a try, but is somehow always right under all circumstances. ;)
Anonymous

Here is a sample: http://theorymine.co.uk/?go=certificate_example

Here is the Theory behind TheoryMine: http://tinyurl.com/27uukjv
Anonymous

Here’s an example theorem:
http://www.newscientist.com/articleimages/dn19809/1-you-too-can-get-that-pythagoras-feeling.html
- Anonymous
  
  TheoryMine generates novel data-types, i.e., new kinds of mathematical object. These data-types are filtered to remove any well known ones, such as numbers, lists, etc. It then creates new functions on these data-types and theorems about these functions. In this way the mathematical theories in which TheoryMine proves its theorems are novel, since they are about new kinds of mathematical objects. It keeps track of the data-types, functions and theorems to ensure it never generates the same ones twice. So two different sales can never be of the same theorem.
  
  Of course, there is no guarantee that someone, somewhere did not previously invent these data-types, functions and theorems — TheoryMine can only filter out those it already knows about. That’s why anyone who is inadvertantly sold a previously known theorem will get two new ones. And TheoryMine will be able to filter these data-types in future.
Cowicide

Hurts brain. Do not understand.
Alan Bundy

Those last two anon posts were from me. I should have created this account before posting them. As a founder of TheoryMine, I don’t want to send anon posts to this blog about TheoryMine.
Anonymous

I’m wondering how they make sure a theorem hasn’t already been previously discovered, since there are many that were discovered before the site was released. It’d be bad if multiple people owned a theorem.
- Anonymous
  
  I would assume that all the theorems they discover are so incredibly jejune that no one has ever taken the time to prove them. So, it’s kinda like setting a new world record for the amount of apple pie eaten while rollerskating in a Walmart parking lot. It’s easy to find a new theorem to prove – the hard part is finding an interesting theorem to prove. What I do wonder is why they are doing this. Godel’s incompleteness theorems basically say “doing something like this is silly”.
desiredusername

It’s still not as cool as coming up with the theorem by actually doing the work.
Anonymous

What a great Christmas present this would make for the mathematician who has everything.
- Anonymous
  
  A mathematician that has everything already has a theorem named after him, one that he earned himself which is infinitely more awesome.
  - Anonymous
    
    He or she!
oasisob1

You can also get a star named. Both databases/registries are of equal value.
Anonymous

I would guess it is very hard for a computer to check if any of those theorems (a.k.a. true statements) are simple corollaries of known theorems.
StAlfongzo

I thought this was kinda cool until I read further. Then I see that the professor is Al Bundy! Oh Al!
Frank_in_Virginia

“For a mere $15″

The Web site says Â£15.00.
Anonymous

What about this… from their site: “You acknowledge that we are the owner or the licensee of rights (including all intellectual property rights) in or relating to our site, the Products, Services, Material and all Theorems.” So I don’t own a theorem? I can’t publish it? I just bought the naming rights?
jphilby

My theory is that paying for unofficial naming of computer-generated theories ranks right up there with paying for star-names, or paying for a Citizen’s Band handle, or winning a square inch of land in Alaska.

Somehow I don’t think this enterprise will be much appreciated by the professional math community. I hope these coke-sniffers, or ex-bankers, or both, go broke running their cute scam.
- Marktech
  
  I hope these coke-sniffers, or ex-bankers, or both, go broke running their cute scam.
  
  Close – one of them’s a professor at Edinburgh University.
  
  http://homepages.inf.ed.ac.uk/bundy/
Anonymous

I see what’s going on here. They’re actually secretly amassing (generating) evidence of Stigler’s law of eponymy. Brilliant.
Anonymous

The way uniqueness is ensured is by constructing new inductively defined sets; this doesn’t guarentee it, but TheoryMine also filters out known sets using digital libraries of formalised mathematics. See: http://www.cl.cam.ac.uk/research/hvg/Isabelle/

On the discover page there is written:

“Theorems are discovered by our robot mathematicians, we make every effort to ensure that the discovered theorems have never been published before, and we guarantee that every theorem we discover has not been previously recorded in our database of theorems. In the unlikely event that that there is a mathematics article publishing the theorem prior to our discovery, then we will give two additional new theorems to the owner of the old theorem.”

It’s very different from naming stars in that mathematics has a long history of the first person to discover a theorem naming it. TheoryMine also checks against existing libraries of mathematics, where star-naming companies do not.
drog

Their software isn’t formally proven to be correct. They pretty much say this in their FAQs, under “HOW CAN I BE SURE THAT THE PROOF OF MY THEOREM IS CORRECT?”

Even if it was, the hardware would need to be formally proven correct as well. That’s the big problem with most computer generated theorems. They lack rigor and therefore aren’t actually theorems.
- Lucas
  
  Generally computer-mechanised and checked proofs are the most trusted mathematical proofs in the world. For example, Intel, AMD, Rockwell, and all other major chip designers use them to verify every floating point unit (the thing that went terribly wrong with the old Pentium). No interesting formal system can prove its own consistency, so that would be a foolish thing to require of a formal proof system: you’d be talking about elaborate descriptions of the empty set! What is done instead is a pen-and-paper proof of the logical consistency, and then use of type systems, and some careful eye-balling and testing to ensure the kernel of a proof system is correct. That plus 20 years of use or so, and its hard to see how you can get much more convincing than that. Of course, that says nothing about learning something interesting from the proof!
nprnncbl

Quentin should get two more theorems named after him, as Quentin’s Theorem is equivalent to stating the associativity of addition.

T defines a type which is equivalent to (Bool,Bool,Nat); since mw ignores its Boolean arguments, in this context T is equivalent to a natural number.

C1(bool,bool) â†” 0
C2(x) â†” 1+x [or Successor(x), from Peano]
T = C1(bool,bool) | C2(T) â†” Nat = 0 | Successor(Nat)

mw is equivalent to an inductive definition of addition on the natural numbers:

mw(C1(b1,b2),y) = y â†” 0 + y = y
mw(C2(x),y) = C2(mw(x,y)) â†” (1+x) + y = 1 + (x+y)

Then we have Quentin’s Theorem:

mw(mw(x,y),z) = mw(x,mw(y,z)) â†” (x + y) + z = x + (y + z).

If this example demonstrates the degree to which they check if a theory is already known, or is useful, then I’d agree that it’s worthwhile as having a star named after you.
- Anonymous
  
  Your observation is that there is homomorphism from mw to addition. But you are wrong to say that mw is equivalent to natural number addition: mw is not commutative; addition is. These are quite different mathematical objects.
- Lucas
  
  No, mw is not equivalent to an inductive definition of addition; mw is not commutative: “mw(x,y) =/= m(y,x)” but “x+y = y+x”. Your hasty observation is that there is a homomorphism from mw to the usual addition on naturals; which is a totally different thing to saying this is a rediscovery of a known function and property.
  - nprnncbl
    
    You’re right about it only being homomorphic, which I noticed after posting; read “equivalence” as homomorphism, and change the arrows to one way. But if my hasty observation is apparently so trivial to you, and you’re correctly able to deduce the non-commutativity of mw so quickly, then I’m not sure why you think this isn’t just a rediscovery. Although I’m also not sure if you’re just joking.
    
    For those following along, mw fails to be commutative because it preserves the Boolean components of its second argument, but not its first. So under the equivalence of T to (Bool,Bool,Nat), we could restate it as
    
    mw((x1,x2,x3),(y1,y2,y3)) = (y1,y2,x3+y3).
    
    In this domain, we also have that 0 (as C1(a,b) for any boolean a,b) is only a left identity: mw(0,x)=x, but not a right identity: mw(x,0)=/=x. We also have mw(x,mw(y,z)) = mw(y,mw(x,z)), a hybrid associative-commutative property that is also true in natural numbers. But are any of these interesting? Or are these what endymion earlier worried about as being trivially true?
    
    If QT is an interesting result, then there’s any number of minor modifications to the domain of QT, yielding similar homomorphisms, with similar embeddings of the associativity of addition. If we also had Shmentin’s Theorem, with C1(Bool) instead of C1(Bool,Bool), with a similar modification to the definition of mw, will Quentin object that Shmentin’s Theorem is just a special case of his own, and doesn’t deserve recognition? After how many such repetitions will the result become uninteresting?
    
    Maybe there’s some intrinsic measure of interestingness of a theorem, akin to Kolmogorov complexity, but taking into account the shortest length of both the theorem and its proof.
    - Lucas
      
      While proofs of commutativity for recursive functions typically require induction (which can make finding the proof very tricky!), proofs of non-commutativity only require an example. So it’s much easier to see that “mw” is not commutative than it is to see that its associative.
      
      The argument for the non-triviality is two-fold (described in the FAQ):
      
      1) the theory is not-inconsistent (done by using conservative extensions, which are well known to preserve consistency)
      
      2) the theorems cannot be proved by rewriting alone (in a the technical sense of term-rewriting). Inductive theorem proving is in general undecidable, but with good heuristics, you can do a lot.
      
      Whether these things are ‘interesting’, or not, is a much more complicated question. Interesting in mathematics is a rather subjective thing. I tried for a good while to see if there was a natural way to characterize all theorems that TheoryMine can produce, but as far as I can see there is not (this is an interesting open-question). So it’s hard to say how significant/interesting they the theorems are. Generally, like it says in the TheoryMine FAQ, the theorems are unlikely to be particularly significant, and I’m not sure if people who buy them would recognize it even when they are!
      
      On an even more technical note: the datatypes used are not polymorphic, so there will be some more general theorems that subsume several of the ones TheoryMine produces. It’s an interesting question as to how one might try to automate the process of finding the generalisations. I guess anti-unification could be used. Inspiring this kind of stuff is what I think is cool about TheoryMine.