A Theorem Marketplace: A Modest Proposal
There is a class of problems that can be represented as a problem of searching for a specific hypothesis in a non-trivial hypothesis space. I guess you can think about this category of problems as trying to look for the correct password to your laptop in the vast space of all possible passwords. Another analogy would be training a neural network - because the training process is essentially looking through the space of possible weights of this network. (Although this analogy doesn’t quite work out, because there isn’t a right or wrong configuration of the neural network - it’s just that some are much better than others).
In particular, problems like that are naturally broken into the sub-problems of 1) prioritization/suggestion and 2) verification. In the password analogy, it helps if you have any idea about what might plausibly be the right password - e. g. an existing English word, if the person who set up the password is prone to that sort of mistake. So that’s the suggestion step - you prioritize some passwords that you think stand a higher chance of being the right one.
The verification step, on the other hand, would be just typing in the passwords and seeing if it worked.
Naturally, for different problems, either of these steps can present a difficulty. Perhaps your suggestor is not good enough, and it prioritizes too many hypotheses, or hypotheses that are just not that good. Perhaps your verification process is expensive and time-consuming. Having a better suggestion process helps either way, because it reduces the expected number of verification attempts.
One problem where this analogy works especially well is automatic theorem proving. Given a theorem, one is to find a string that is a correct proof of that theorem. The verification step is rather cheap - there are existing languages and toolsets for writing out theorems and proofs in a formalized way, and for verifying a given proof’s correctness.
The suggestion step, on the other hand, is a nightmare. You simply cannot afford to check every possible string one-by-one, for combinatorial reasons. So you need an intuition about what a reasonable proof of that theorem would probably look like, and this is the type of task that, until recently, was mostly deemed insurmountable to automate.
***
I am saying until recently because we now live in a world with language models; see for example this paper where OpenAI used a language model for generating formal proofs of theorems. It appears that an important civilizational bottleneck - meaningful automation of mathematical progress - has recently gained new vectors of attack. So let’s exploit that!
How do we make it work, though?
I mean, obviously, we can train a language model on Lean or something like that. Or email OpenAI and say “can you pls give us your theorem prover language model”.
That doesn’t quite solve the civilizational bottleneck, though. How do we get from having a better theorem proof suggestor to actually changing the process by which mathematical statements are accepted as proven theorems by the mathematical community?
There is a social process to the creation of knowledge, you see. There is little use to knowledge that is not connected into a system, and available upon request. Perhaps there is a mathematician in Dublin who is missing a key idea for finalizing her work; and a mathematician in Johannesburg who possesses the insight that her colleague is lacking; there will be no use for either’s insights, because they only work when they’re connected.
Well, the approach to navigating social processes that I like can be summed up with one word: incentives. As someone’s bio on Manifold reads: “Incentivize the change you want to see in the world”. There is a wisdom to modeling a social dynamic by assuming people will mostly obey incentives; and it is the wise thing to do to use this principle for designing new systems.
***
How do we incentivize the suggestion step for theorem proving? What’s a way to make people want to solve pretty specialized mathematical problems? We kind of already did that, with incentivizing people to find strings of a particular format whose SHA-256 hash is small enough.
I’m talking, of course, about Bitcoin mining, which is essentially many competing actors trying to solve a specific mathematical problem because whoever gets there first, gets the money.
The difference here is, it’s hard to get better at the task by being smarter about which candidates you try. You just brute-force the search until you stumble upon the right option.
And we don’t have to do it like that with theorem proving. You can get a valid proof first by being smarter.
***
How do you have people get money for theorems?
One approach that has a history in the mathematical community is declaring bounties on theorems. The most famous example is Clay’s institute’s millennium prize problems. The institute pledged a million dollars for each of those problems, to be awarded for the first solution of each. But it’s not just them. Paul Erdős was famously in this habit; famous problems with an “Erdős prize” include the Collatz conjecture and the Erdős conjecture on arithmetic progressions.
So perhaps we should find a way to do it in a unified, standard way, connecting one person’s bottlenecks with another person’s insights, incentivizing the creation of better suggestion processed, in an attempt to unify the knowledge base that has for a very long time been too large for a single head.
***
My modest proposal, then, is for a platform where bounties on theorem proofs can be announced and claimed by whoever presents a valid formal proof first.
So, we have three sides of the question.
Announcing a bounty. This is not meant to be centralized, or done by the platform itself, or anything like that. The idea is to present anyone the opportunity to exchange money for a chance of your mathematical problem being solved - just like with regular bounties. This activity is meant for one half of the audience of the hub.
The suggestion step. This is meant for the other half. This step is automatable, and meant to be automated, probably by training better language models for theorem proving languages like Lean.
The verification step. This step is also meant to be automated, and provided by the platform itself.
(I should probably come up with a fancier name for the bounty announcement - like “the problem-posing step” or some such)
***
I think this idea makes sense. I expect there are many features to try and play around with - for example, with the structure of theorems that are already proven - e. g. If there is a bounty for proving A -> C, and we have a proof that A -> B, then we can just give out the bounty for proving that B -> C? Or perhaps give parts of the bounty to authors of both proofs? In what proportion? Like I said, there are options to play around with.
What I don’t know is how to get anyone to care about it. Your regular mathematician does not use a theorem prover in her career; perhaps this would start as being useful for applications like “a frustrated Lean enthusiast doesn’t know how to prove this extremely basic lemma”. Even so, I don’t know how many people would wish to throw money at theorems like this.
Still, give me a pingback if you want to attack this with me.