The Capitalism of Theory
December 5, 2010 2:50 PM Subscribe
Need a gift for the geek who has everything, or for your know-it-all uncle? How about naming a novel mathematical proof after them? TheoryMine will sell you the naming rights to a proof generated by their software algorithm.
It's hardly the first time it's happened, with the well-known example of L'Hôpital's rule, which was afterwards known to have been discovered by Johann Bernoulli. Nevertheless, Marcus du Sautoy is unimpressed and suggests that the proceeds should go to charity, as in his earlier sale of the names of symmetrical objects in hyperspace.
It's hardly the first time it's happened, with the well-known example of L'Hôpital's rule, which was afterwards known to have been discovered by Johann Bernoulli. Nevertheless, Marcus du Sautoy is unimpressed and suggests that the proceeds should go to charity, as in his earlier sale of the names of symmetrical objects in hyperspace.
I'd really like to see some theorems generated by this software. Do you have any links?
posted by scose at 3:01 PM on December 5, 2010
posted by scose at 3:01 PM on December 5, 2010
Missing link: The Theory behind TheoryMine
posted by Jakey at 3:04 PM on December 5, 2010 [4 favorites]
posted by Jakey at 3:04 PM on December 5, 2010 [4 favorites]
Kind of like that service that's advertised in Readers Digest that names a star after your grandmother and sends her an official certificate and registers it officially with the government (copyrighting the booklet where the name is recorded) for $14.95!
posted by sammyo at 3:10 PM on December 5, 2010
posted by sammyo at 3:10 PM on December 5, 2010
sammyo, RTFA:
"You may think this is an elaborate scam, or that you'll just end up with an obscure equation copied from some long-forgotten textbook, but TheoryMine claims to have far more validity than superficially similar companies selling star names."
posted by strixus at 3:11 PM on December 5, 2010
"You may think this is an elaborate scam, or that you'll just end up with an obscure equation copied from some long-forgotten textbook, but TheoryMine claims to have far more validity than superficially similar companies selling star names."
posted by strixus at 3:11 PM on December 5, 2010
I'm waiting for the automated system that generates algorithms, wraps them in some arbitrary business method, and then patents them.
posted by mullingitover at 3:12 PM on December 5, 2010 [3 favorites]
posted by mullingitover at 3:12 PM on December 5, 2010 [3 favorites]
"You may think this is an elaborate scam, or that you'll just end up with an obscure equation copied from some long-forgotten textbook, but TheoryMine claims to have far more validity than superficially similar companies selling star names."
Is there any data to back up these claims?
posted by FuzzyLumpkins at 3:24 PM on December 5, 2010
Is there any data to back up these claims?
posted by FuzzyLumpkins at 3:24 PM on December 5, 2010
Man, I wanna get a bunch of these for everyone in my office who opens up their computer's calculator to figure out the correct change for a $12.50 lunch delivery order, but my poorly developed proto-conscience is tingling in what is perhaps a significant fashion.
It also might just be gas, idk.
posted by elizardbits at 3:28 PM on December 5, 2010
It also might just be gas, idk.
posted by elizardbits at 3:28 PM on December 5, 2010
Er. Change from a $20, that is.
My smartypants appear to have given me a wedgie.
posted by elizardbits at 3:29 PM on December 5, 2010
My smartypants appear to have given me a wedgie.
posted by elizardbits at 3:29 PM on December 5, 2010
So what they do is they define a type like this one:
A_Number ::= Zero | One_More_Than(A_number)
This is the natural numbers (or their shadows). 3 is written
One_More_Than(One_More_Than(One_More_Than(Zero)))
You can define addition, substraction, etc. on it, and prove their properties. What they do is that they add parameters to the types, like in their example:
T ::= C1(Bool,Bool) | C2(T)
They then generate simple functions that are a bit like addition and substraction on the naturals, and conjectures on these functions. For instance, in the linked theorem, the program has conjectured that an addition-like function is commutative.
They make a bunch of these conjectures, then eliminate some by using Quickcheck to find counterexamples. They then feed the possible theorems into the Isabelle theorem prover, which they drive (theorem provers are notoriously difficult to use) using a program they wrote that can find proofs for a lot of those theorems.
Since once a proof is found it's verified by a small kernel program that has been thoroughly inspected by specialists, we can be reasonably confident that the theorems are indeed true.
posted by Monday, stony Monday at 4:20 PM on December 5, 2010 [3 favorites]
A_Number ::= Zero | One_More_Than(A_number)
This is the natural numbers (or their shadows). 3 is written
One_More_Than(One_More_Than(One_More_Than(Zero)))
You can define addition, substraction, etc. on it, and prove their properties. What they do is that they add parameters to the types, like in their example:
T ::= C1(Bool,Bool) | C2(T)
They then generate simple functions that are a bit like addition and substraction on the naturals, and conjectures on these functions. For instance, in the linked theorem, the program has conjectured that an addition-like function is commutative.
They make a bunch of these conjectures, then eliminate some by using Quickcheck to find counterexamples. They then feed the possible theorems into the Isabelle theorem prover, which they drive (theorem provers are notoriously difficult to use) using a program they wrote that can find proofs for a lot of those theorems.
Since once a proof is found it's verified by a small kernel program that has been thoroughly inspected by specialists, we can be reasonably confident that the theorems are indeed true.
posted by Monday, stony Monday at 4:20 PM on December 5, 2010 [3 favorites]
I will name the next piece of policy research I do after someone for $20. Just imagine:
Janus Luxembourg: Budgetary Effects of Replacing 8" Traffic Light Bulbs with 12" Bulbs.
The City of Reno will spend millions on the light from thousands of bulbs. But for $20 you can have all that light in her smile on Christmas morning.
posted by munchingzombie at 4:30 PM on December 5, 2010 [2 favorites]
Janus Luxembourg: Budgetary Effects of Replacing 8" Traffic Light Bulbs with 12" Bulbs.
The City of Reno will spend millions on the light from thousands of bulbs. But for $20 you can have all that light in her smile on Christmas morning.
posted by munchingzombie at 4:30 PM on December 5, 2010 [2 favorites]
Given an n-dimensional fruitcake...
You can recycle it before you get it. (Link to a friend's silliness)
posted by cjorgensen at 6:29 PM on December 5, 2010 [2 favorites]
You can recycle it before you get it. (Link to a friend's silliness)
posted by cjorgensen at 6:29 PM on December 5, 2010 [2 favorites]
I'd feel a whole lot better about whether their theorems were reliably correct had they, y'know, spelt "Pythagoras" correctly.
posted by randomination at 8:09 PM on December 5, 2010 [1 favorite]
posted by randomination at 8:09 PM on December 5, 2010 [1 favorite]
I can prove my own theorems. Maybe I should start giving them as gifts to my friends?
posted by madcaptenor at 9:33 PM on December 5, 2010
posted by madcaptenor at 9:33 PM on December 5, 2010
I get that they do indeed create correct theorems...but I'd like one I purchased from them to be at least somewhat potentially useful to the world.
Even "named stars" could have resources, or even life! What good are these auto-generated theorems?
posted by swimming naked when the tide goes out at 11:09 PM on December 5, 2010 [1 favorite]
Even "named stars" could have resources, or even life! What good are these auto-generated theorems?
posted by swimming naked when the tide goes out at 11:09 PM on December 5, 2010 [1 favorite]
I got you a truly marvelous present! Unfortunately, this stocking is too small to contain it.
posted by moonmilk at 11:10 PM on December 5, 2010 [2 favorites]
posted by moonmilk at 11:10 PM on December 5, 2010 [2 favorites]
Mathematicians rarely have any idea how useful their theorems are going to be. Georg Cantor didn't expect we'd be able to observe any infinities, but he made theorems about them anyway.
posted by LogicalDash at 3:36 AM on December 6, 2010
posted by LogicalDash at 3:36 AM on December 6, 2010
Personally, I'd prefer something based on Doron Zeilberger's methods for automated discovery and proof of combinatorial identities.
posted by mhum at 9:48 AM on December 6, 2010
posted by mhum at 9:48 AM on December 6, 2010
I dabbled a little in automated theorem proving back in the day. It gives me a warm glow to know that Alan Bundy is still working, he must be getting on for 70 now.
But from the looks of that example theorem, it doesn't look like the field has advanced very far though. Which seems to be the story of AI generally too.
I'd like one I purchased from them to be at least somewhat potentially useful to the world.
It looks like the theorems are about fairly arbitrary formal systems, so the chances of them being especially useful aren't great. The theorems also probably wouldn't be very hard for a person to prove, but it would be too boring and time-consuming for people to churn out lots of small theorems about such systems.
posted by philipy at 10:21 AM on December 6, 2010
But from the looks of that example theorem, it doesn't look like the field has advanced very far though. Which seems to be the story of AI generally too.
I'd like one I purchased from them to be at least somewhat potentially useful to the world.
It looks like the theorems are about fairly arbitrary formal systems, so the chances of them being especially useful aren't great. The theorems also probably wouldn't be very hard for a person to prove, but it would be too boring and time-consuming for people to churn out lots of small theorems about such systems.
posted by philipy at 10:21 AM on December 6, 2010
One of my geek friends has dropped hints that he wants one of these for Xmas, which is fine by me. £15 for a theorem he can hang on his wall instead of some CD that'll be forgotten in a year makes for a decent gift, usefulness of the theorem or not.
My question to you math brainiacs out there: calling it "x's theorem" is kind of boring. The thesaurus has lots of options:
assumption, axiom, belief, deduction, dictum, doctrine, formula, fundamental, law, postulate, principium, principle, proposition, rule, statement, theory, thesis.
Would it be appropriate to substitute any of these words for "theorem" and not offend my geek friend's sense of mathematical propriety? I am particularly fond of axiom.
posted by Chichibio at 2:34 AM on December 9, 2010
My question to you math brainiacs out there: calling it "x's theorem" is kind of boring. The thesaurus has lots of options:
assumption, axiom, belief, deduction, dictum, doctrine, formula, fundamental, law, postulate, principium, principle, proposition, rule, statement, theory, thesis.
Would it be appropriate to substitute any of these words for "theorem" and not offend my geek friend's sense of mathematical propriety? I am particularly fond of axiom.
posted by Chichibio at 2:34 AM on December 9, 2010
You might be able to get away with "law", but the others have very different meanings to "theorem" to anyone that knowns what that really means.
In this context "axiom" is definitely not the same as theorem. A set of axioms would be like the ingredients you gave to a chef, and the theorem would be the fine meal they made from them.
So if you're a mathematician, "theorem" doesn't sound boring. X's Theorem has the same kind of ring to it as X's Cello Concerto would for a composer.
posted by philipy at 10:37 AM on December 9, 2010 [1 favorite]
In this context "axiom" is definitely not the same as theorem. A set of axioms would be like the ingredients you gave to a chef, and the theorem would be the fine meal they made from them.
So if you're a mathematician, "theorem" doesn't sound boring. X's Theorem has the same kind of ring to it as X's Cello Concerto would for a composer.
posted by philipy at 10:37 AM on December 9, 2010 [1 favorite]
Thanks philipy. I definitely wouldn't want to screw that one up with this particular, much-beloved math/science nerd. The kind that does calculus problems for fun.
If "theorem" is as awesome as you make it out to be, perhaps I can play around with the format, like "The [last name] Theorem".
Could I get away with "[last name]'s Theorem of Love"?
posted by Chichibio at 5:46 AM on December 11, 2010
If "theorem" is as awesome as you make it out to be, perhaps I can play around with the format, like "The [last name] Theorem".
Could I get away with "[last name]'s Theorem of Love"?
posted by Chichibio at 5:46 AM on December 11, 2010
Theorems vary in significance and difficulty, but if one is named, esp after a person, that normally means it's at the important end of the scale, and would likely be the result of months or years of work, and a major contribution to the field it was about.
The theorems this system turns out won't be significant like that, but the kick people would get out of having a theorem named after them would be because of that association.
Could I get away with "[last name]'s Theorem of Love"?
That depends on their sense of humor. Obviously the theorem you get isn't actually going to be about love, but that kind of thing would appeal to some people. You know this guy, so you can probably judge.
You might get some ideas from the Wikipedia entry on theorem terminology. You might able to use Rule, Law or Principle instead of "Theorem".
Some super-important theorems have the word "fundamental" in them, so you might want to work that in somehow.
If anyone really had worked out the Fundamental Theorem of Love, I'm sure we'd all want to know what it was. :)
posted by philipy at 10:50 AM on December 11, 2010
The theorems this system turns out won't be significant like that, but the kick people would get out of having a theorem named after them would be because of that association.
Could I get away with "[last name]'s Theorem of Love"?
That depends on their sense of humor. Obviously the theorem you get isn't actually going to be about love, but that kind of thing would appeal to some people. You know this guy, so you can probably judge.
You might get some ideas from the Wikipedia entry on theorem terminology. You might able to use Rule, Law or Principle instead of "Theorem".
Some super-important theorems have the word "fundamental" in them, so you might want to work that in somehow.
If anyone really had worked out the Fundamental Theorem of Love, I'm sure we'd all want to know what it was. :)
posted by philipy at 10:50 AM on December 11, 2010
« Older Figment | mcmyspace angle Newer »
This thread has been archived and is closed to new comments
posted by RobotVoodooPower at 2:56 PM on December 5, 2010 [2 favorites]