Are mathematicians just not trying hard enough?
The Riemann hypothesis is one of the most important open problems in math. There’s a $1 million prize from the Clay mathematics institute for a proof or disproof of the Riemann hypothesis. At the time of writing, it remains unsolved. From this, we may conclude that one cannot simply buy a solution to difficult mathematical problems.
Or could we? How do we know that buying a difficult maths proof is impossible? Perhaps the Clay mathematics institute is somehow not asking the question in the right way. And it’s true that the value of a million dollars has been eroded over time by inflation. One might guess that a Riemann proof would be worth at least 100 million. Would that be enough to conjure it from the collective intelligence of humanity?
Simply directly declaring a $100 million reward for a solution would probably not work. For one thing, there’s the issue of corollary-sniping where the prize wouldn’t give anyone an incentive to publish solutions to hard intermediate steps of the problem, since the prize as a whole only goes to the one who solves the entire problem as a whole. For another, even the million dollar prize on its own would be plenty of reason for a money-motivated person to solve the problem if a solution were within their grasp. The issue is not merely one of funding, we humans are somehow failing to combine our efforts properly.
Prediction markets are pretty cool
One of the standard ways to buy knowledge is prediction markets. Can we try that here? John Wentworth describes here a scheme for using markets to get mathematical proofs. Here’s a scheme that’s very similar in the overall idea, though the exact rules are slightly different:
Shares on mathematical propositions are traded on the market. Propositions should be the kind of things that might be theorems, i.e. they are syntactically meaningful, and contain no free variables, though it’s fine if they are false or unprovable.
Shares on provable propositions are worth $1, at least if anyone knows or can find the proof. How this works out in practice is that a share in can be redeemed in exchange for $1, together with the next rule.
Shares in logically equivalent propositions can be exchanged for each other. So if it’s the case that then a share in can be exchanged for a share in . This is a trading rule that will obviously have to be called the Law of Equivalent Exchange. We only allow exchanges that can be seen to be equivalent in one step, but for anything that can be proved equivalent in any number of steps, we can simply make multiple exchanges to get the shares we want.
How do people get these shares they’re trading to begin with? Simple! You can buy shares in for $1. You can also buy shares in for $0, i.e. they’re free.
We allow traders to perform a logical share splitting operation. This is a special operation that is described in the next section.
As Wentworth explains, the virtue of this system is that in order to redeem shares for a proposition you can prove, you need to reveal your proof to the people running the market. Not to other traders necessarily, but whatever the market mechanism is that is enabling the above rules, it can see the math proofs implied in the trades people make.
Logical share splitting
A common theme in mathematics is to split proofs up like this: First we show , then we show . This allows us to prove . Part of the point of using a market is to combine the intelligence of the various traders in the market into something greater than any individual trader. So ideally, we’d like to be able to prove , even if one trader can only prove and the other trader can only prove . So let’s say there’s some profit in proving : Shares are trading at less than $1 (say $0.6), but we could redeem them for $1 if we could only prove . Alice knows how to prove (redeem shares for) . Bob knows how to prove (redeem shares for) . How can they make money?
Logical share splitting provides a way. It works by permitting the exchange of a pair of shares for a different pair of shares in such a way that the possible payout of redeeming the shares remains unchanged. This is a new share exchange rule, it isn’t possible to make an equivalent trade using any of the previously described rules. The rule:
For any two propositions , logical share splitting allows a share in and a share in to be exchanged for a share in and a share in . This exchange can go in either direction.
The logic behind why payouts remain the same is as follows: Consider how many of the propositions are true. The number is 0, 1, or 2. If neither is true, then the shares in each are worth nothing, and the combined shares are also worth nothing. If one is true and one is false, then the combined share is worth $1, while the combined share is worth nothing. Finally, if both are true, then each of the combined shares is worth $1.
So now let’s see how Alice and Bob can make money on shares in by combining their proofs of and . First Alice, who can prove , produces many many shares of for free. This is doable if you have a proof for by starting from a bunch of free shares and using equivalent exchange. She sells these for $0.2 each to Bob, pure profit. Then Bob purchases many many shares of . These are not purchased from the market mechanism, which only sells or shares, but rather on the open market, which in this scenario prices them at $0.6. Given a share each of and , logical share splitting then allows exchanging them for and . The latter shares are worthless, since we know that is true. But the former shares are equivalent to and since Bob has a proof of this, they can be redeemed for $1. This gives a profit of $0.2 for Bob. Alice and Bob’s combined profits come to $0.4, exactly the difference between the $0.6 price of shares in and the $1 they should be worth, given that has a proof.
(It’s important to note that logical share splitting wasn’t required to make this work. After all, Alice and Bob together had a proof of so they could have just passed shares back and forth between them, conjoining their sub-theorems as required and removing them after they were no longer needed. Logical share splitting just allows each of them to know less about what the other is doing. For all Bob knew, Alice could have been speculating that would turn out to be true, rather than actually having a proof. And it’s possible that Alice had no idea when trading with Bob that Bob was trying to prove . In short: It’s nicer if the fact that is provable is reflected in a low price for shares rather than a low price for providing the service of sticking an “” onto arbitrary shares. Also, because the market mechanism only sells true or false shares, it’s important to have a way to construct shares in other propositions besides proving them.)
A special case of logical share splitting is to use the law of excluded middle to mint shares on various propositions. For example, given $1, we can buy a share in and while we’re at it, we’ll pick up a share in for free. Then using equivalent exchange (and the law of excluded middle), these can be converted to shares in and for an arbitrary choice of proposition . Then using logical share splitting (in reverse this time), these can be converted to shares in and . Individually, these shares might have any value, but we know that the sum of their values must be $1, exactly because this trade is possible. Robin Hanson dubbed trades that convert money to shares in a proposition and its negation “splits” (to avoid confusion, we’re calling this “minting”) and the reverse kind of trade “joins”. With the ruleset above, such operations can be decomposed into their more fundamental components: Equivalent exchange (with law of excluded middle), and logical share splitting.
Computer Assistance
In theory, any mathematician throughout history with an understanding of formal logic could have run a market of this kind. However it would be a huge amount of work to manually make and verify all trades, for relatively little benefit. A computerized market, with a well-defined API, is much more useful. We should imagine that most trades on such a market will be made by computers. Proof languages like Coq, as well as automatic theorem provers seem likely to be heavily used here. In addition, fully formal rigorous proofs are labour-intensive for mathematicians to write down, so large language models could provide a good way to convert informal proofs and arguments into the format expected by the proof system. Machine learning in general might have many interesting applications here.
Application to Ordinary Prediction Markets
While previously we’ve been describing a mathematical use case, there’s no reason that we couldn’t also include atomic shares corresponding to the outcomes of real world events. Then these could be combined logically just like questions in mathematics. For example, if corresponds to “the next US president will be a Republican” and corresponds to “the next US vice-president will be a Democrat”, then shares could be minted for using the usual excluded-middle share-minting technique. And while both and shares might be trading at middling values, shares would be trading for very little, which tells us that the events corresponding to and are not independent.
Ordinary prediction markets deal in individual events, but there’s no extra cost to allowing logical combinations of events. So long as we’re able to resolve the outcome of each prediction, that tells us how to resolve all logical combinations. Here’s the extra trading rule we’ve got to add:
If a prediction resolves to true, then from that point forwards, we allow traders to replace with anywhere it appears in a logical expression. Similarly, if it resolves to false, we thereafter allow replacing with . This can be considered a special case of Equivalent Exchange. Like all other trading rules, this rule is reversible, though there’s not much point in using the reversed version of this particular rule.
In the simplest case, this rule allows converting shares in to shares in if event happened, and thus redeeming them for $1.
Application: Conditional prediction markets. Say you’re trading in several conditional prediction markets, conditional on an event . Perhaps you want to make $100 bets on predictions given and given . The way an ordinary prediction market handles conditional predictions is to resolve to N/A when the event we’re conditioning on doesn’t happen. When a market resolves N/A, it means that all the traders get the money they invested back. So if I were betting on an ordinary prediction market (Manifold, say), I’d have to put up $200 in capital to make my bets. Even though only one of those two markets would ever resolve at all. The other would just give me my $100 back again.
Intuitively it seems like making those bets should only require $100 of capital, since and are mutually exclusive, and whichever of the two happens to be true, I’m then only investing $100. If you’ve ever bet in conditional prediction markets, you may have wished that you could make investments on both sides of the conditional without the required capital needlessly doubling. Markets with logical share splitting allow this.
The way conditional prediction markets work with this ruleset is as follows: To bet on given , I buy shares in . But I don’t buy them with dollars. Buying with dollars would just mean I’m investing in itself. Instead, I buy them with shares in . There must be some going-rate at which other traders are willing to give me shares in in exchange for shares in and it’s exactly this rate that gives the conditional market price. Now to make my investment, I don’t need $200. Instead I can spend $100 to mint 100 shares of and 100 shares of . Then I can invest in with my shares and in with my shares. Note that if I just hold on to my shares for rather than investing them, then we’re back at Robin Hanson’s original formulation of what it means to invest in a conditional: I get my investment back if doesn’t happen.
Subsidizing the Market
In our example above, Alice and Bob were driven to prove because its shares had a price of only $0.6, even though it was provable. It’s well known that in order to run a prediction market, it must be subsidized, where prices in a proposition and its negation sum to slightly less than $1. Otherwise, trading in the market is a zero-sum game and participants would on average have no reason to play. Therefore, the people who want to know the answer for a particular question have a reason to subsidize the market for that question.
But wait a second: Suppose that we’re subsidizing the market in so that prices for and sum to $0.99, say, instead of $1. This permits an arbitrage: Buy shares in and from the subsidizers for $0.99, and then do a join to get $1 out, for a profit of $0.01. This is not what we wanted, we’re basically just giving away pennies for free. As subsidizers, we’re fine with losing money on the deal, but we want that money to end up stuck in shares that can only be redeemed by actually proving the proposition we’re interested in. If traders can make a profit right away by just cancelling out all their shares with each other, that doesn’t accomplish our goal.
We might be able to get around this by talking about proofs instead of propositions directly. In other words, we could request a proof or disproof of the Riemann hypothesis by separately subsidizing shares in and . These are not the negations of each other, so they can’t be cancelled out. The market mechanism just auctions off a bunch of shares without counter-balancing shares. And these auctioned shares can then only be redeemed by proving the Riemann hypothesis. Or, at least by proving that the Riemann hypothesis has a proof. There’s a chance that someone might find a non-constructive proof of , though it’s possible for human observers outside the system to decide they’re willing to extend their axioms so that such non-constructive proofs of would themselves count as proofs of .
Appendix: Completeness
It turns out that these laws of trading are complete in the sense that they allow the conversion of any set of shares into any other set of shares of equivalent value. Where equivalent value means that the two sets of shares can be redeemed for the same amount of money, regardless of how all the underlying propositions resolved. (The setup here is that we have some underlying propositions, each of which can be either true or false. These could be prediction market predictions, or (though the math here would be kind of poorly-defined) they could be propositions that do not yet have proofs or disproofs.)
For ease of understanding, I’ll give a “proof” by example. Suppose that is some expression of the propositions . Then we can express it in disjunctive normal form. Say it comes out as: . For short, we’ll define so that . We’ll call the expressions “one-hot” expressions, since they’re each true for exactly one of the possible outcomes. We can convert a share in into shares in the underlying one-hot expressions as follows:
start from
buying false is free
equivalent exchange (different one-hot expressions are contradictory)
logical share splitting
We can repeat the process until we have shares in each separate one-hot expression.
buying false is free
equivalent exchange
logical share splitting
We can convert a share in any logical expression into its component one-hot expressions like this. By applying the conversion to all shares in the set, we can convert any set of shares into an equivalent set of one-hot shares. Because all laws of trading are reversible, this means we can convert any set of shares into any equivalent set by first converting to the equivalent set of one-hot shares, and then converting to the desired share set.
Appendix: See Also
This is all closely tied to the theorem in probability that . The concept of a valuation also seems to be very related.
I think this is a suitable mechanism for grants for well defined mathematical problems, but not for more vaguely defined ones. To be frank, the well defined ones tend to be less interesting.
For example the Cray problems are all well defined, and are certain very interesting, but mostly not actually that fundamental to mathematics.
The Hilbert problems are in some ways far more important, and most of these are more vague questions or directions for research than an actual concrete conjecture.
Nobody would have been trading shares in godels incompleteness theorem before he proposed it—and rendering the theorem in concrete terms would already be halfway towards solving it.
How would you suggest making sure funding gets pointed towards these kinds of problems as well?
However we currently do it, I guess; I don’t have any improvements in this particular direction. Though do note that P vs NP, and P vs PSPACE, and BQP vs P or NP are all examples of precisely-defined problems that are also very significant. These are problems that I would much rather have an answer for than the Riemann hypothesis. Though even there, the process isn’t guaranteed to generate an interpretable proof.
If it didn’t directly yield a solution, I think it would produce a huge leap forward. That’s a huge sum of money. Syndicates would form, and some would be competent.
As for your and John’s schemes, I didn’t try to understand them, but they seem to be heavy on logical formalism. But you shouldn’t overestimate the importance of deductive formalism in fundamental mathematical research. Creativity and ingenuity are the truly essential ingredient.
Did you reach the section on computer assistance yet? The idea is that mathematicians could use their creative insight as normal, write up a paper as normal (minus a lot of effort spent on polishing), and then ask GPT-4 or a successor to convert that into the corresponding low-level formalism. I get the sense that we’re only just passing (or are about to pass) the technology threshold where it could possibly make sense to do things this way. The market idea does have several advantages:
Formal reasoning means that proofs produced in this way do not contain errors.
Non-mathematicians can participate (for smaller leaps of reasoning than the ones requiring lots of creativity and deep mathematical intuition).
Reinforcement learning algorithms can participate.
GOFAI algorithms can participate.
Better combination of insights from all these participants.
Automatically creates prediction markets on conjectures.
Very speculatively: Might have some application as a variant of logical induction?
The main drawbacks are:
Doesn’t necessarily produce interpretable proofs.
Profit-motivated participants have to keep their proofs secret, maybe for a long time if they expect most of the supply for the shares they can redeem to appear a long ways into the future.
As you say, overhead from formalism.
Of course, even if you think all this math stuff isn’t interesting, the application to ordinary prediction markets allows double-investing in conditional markets, which I think is pretty nice.
This is very neat work, thank you. One of those delightful things that seems obvious in retrospect, but that I’ve never seen expressed like this before. A few questions, or maybe implementation details that aren’t obvious:
For complicated proofs, the fully formally verified statement all the way back to axioms might be very long. In practice, do we end up with markets for all of those? Do they each need liquidity from an automated market maker? Presumably not if you’re starting from axioms and building a full proof, and that applies to implications and conjunctions and so on as well, because the market doesn’t need to keep tracking things that are proven. However:
In order for this to work, the market must be willing to maintain a price for these shares in the face of a proof that they’re equivalent to ⊥. Presumably the proof is not yet public, and if Alice has secret knowledge she can sell with a profit-maximizing strategy.
She could simply not provide the proof to the exchange, generating A and ¬A pairs and selling only the latter, equivalent to just investing in A, but that requires capital. It’s far more interesting if she can do it without tying up the capital.
So how does the market work for shares of proven things, and how does the proof eventually become public? Is there any way to incentivize publishing proofs, or do we simply get a weird world where everyone is pretty sure some things are true but the only “proof” is the market price?
If there are a large number of true-but-not-publicly-proven statements, does that impose a large computational cost on the market making mechanism?
Second question: how does this work in different axiom systems? Do we need separate markets, or can they be tied together well? How does the market deal with “provable from ZFC but not Peano”? “Theorem X implies corollary Y” is a thing we can prove, and if there’s a price on shares of “Theorem X” then that makes perfect sense, but does it make sense to put a “price” on the “truth” of the ZFC axioms?
Presumably if we have a functional market that distinguishes Peano proofs from ZFC proofs, we’d like to distinguish more axiom sets. What happens if someone sets up an inconsistent axiom set, and that inconsistency is found? Presumably all dependent markets become a mess and there’s a race to the exits that extracts all the liquidity from the AMMs; that seems basically fine. But can that be contained to only those markets, without causing weird problems in Peano-only markets?
Probably some of this would be clearer if I knew a bit more about modern proof formalisms.
Thanks! I’ll try to answer some of your questions.
In practice, I think not. I expect interesting conjectures to end up thickly traded such that the concept of a market price makes sense. For most other propositions, I expect nobody to hold any shares in them at all most of the time. To take the example of Alice and ¬A, if we suppose that Alice is the only one with a proof of A, then everyone else has to tie up capital to invest in A, but Alice can just create shares of ¬A for free, and then sell them for profit. If A is an interesting conjecture, then Alice can sell on the open market and Bob can buy from the open market. If A is a niche thing, only useful as a step in the proof of B, then Bob might trade directly with Alice and the price will be determined by how hard Bob would find it to come up with a proof of A himself, or to find someone other than Alice to trade with. So Alice does have to keep her proof secret for as long as she wants to profit from it.
Different axiom systems can encode each other. So long as we start from an axiom system that can fully describe Turing machines, statements about other axiom systems should be possible to encode as statements about certain specific Turing machines. The root system has to be consistent. If it’s inconsistent, then people can just money pump the market mechanism. But systems built on top need not be consistent. If people try to prove things about some pet system that they’ve encoded, and that system happens to be inconsistent, that means that they’re surprised by the outcomes of some markets they’re trading on, but it doesn’t blow up the entire rest of the market.
I expect that the computers running this system might have to be fairly beefy, but they’re only checking proofs. Coming up with proofs is a much harder task, and it’s the traders who are responsible for that. Sorry if this is a bad answer, I’m not 100% sure what you’re getting at here.
For thickly traded propositions, I can make money by investing in a proposition first, then publishing a proof. That sends the price to $1 and I can make money off the difference. Usually, it would be more lucrative to keep my proof secret, though. So I think we do actually get this weird world you’re talking about. The market mechanism can see all the proofs everyone is using, of course, but people wouldn’t want to trade with a market mechanism that would blab their proofs everywhere. We can imagine that the market mechanism does reveal the proofs, but only after 10 or 20 years so that the discoverer has had plenty of chance to make money.
I think that knowing which things are true even if you don’t know why does still contribute something to mathematical progress, in a weird way. There’s a trick in theoretical comp-sci where a program that tells you whether a given SAT problem is solvable can be run repeatedly (only a linear number of times) to give an actual concrete solution to that SAT problem. You try setting the first variable to 0, leaving all the others free. If the problem is still solvable, you set it to 0. Otherwise, you set it to 1. Repeating this process gives a full solution to the SAT problem. Something similar might be possible for proofs.
Thank you! Much to think about, but later...
They’re not, though. They’re making markets on all the interrelated statements. How do they know when they’re done exhausting the standing limit orders and AMM liquidity pools? My working assumption is that this is equivalent to a full Bayesian network and explodes exponentially for all the same reasons. In practice it’s not maximally intractable, but you don’t avoid the exponential explosion either—it’s just slower than the theoretical worst case.
If every new order placed has to be checked against the limit orders on every existing market, you have a problem.
The problem I’m imaging comes when the market is trading at .999, but life would really be simplified for the market maker if it was at actually, provably 1. So it could stop tracking that price as something interesting, and stop worrying about the combinatorial explosion.
So you’d really like to find a world where once everyone has bothered to run the SAT-solver trick and figure out what route someone is minting free shares through, that just becomes common knowledge and everyone’s computational costs stop growing exponentially in that particular direction. And furthermore, the first person to figure out the exact route is actually rewarded for publishing it, rather than being able to extract money at slowly declining rates of return.
In other words: at what point does a random observer start turning “probably true, the market said so” into “definitely true, I can download the Coq proof”? And after that point, is the market maker still pretending to be ignorant?
There’s no reason I can’t just say: “I’m going to implement the rules listed above, and if anyone else wants to be a market-maker, they can go ahead and do that”. The rules do prevent me from losing money (other than cases where I decide to subsidize a market). I think in some sense, this kind of market does run more on letting traders make their own deals, and less on each and every asset having a well-defined price at a given point in time. (Though market makers can maintain networks tracking which statements are equivalent, which helps with combining the limit orders on the different versions of the statement.)
Good question, I’m still not sure how to handle this.
Actually, I don’t think that creates any problem? Just create shares of “ZFC axioms” and “not ZFC axioms” via logical share splitting. If you are unable to sell “not ZFC axioms”, that only means that price of one main share is $1 (though, it’s likely possible to prove something fun if we take these axioms as false).
Is there any implementation of this? If not, has any thought been put into how one would actually implement this?
I have not implemented it myself, and don’t know of anyone else who has either.
I’d guess in terms of how it would be implemented, the best way would be to piggyback off of Coq or some other language from this list. Many of these already have a lot of work put into them, with libraries of definitions and theorems and so on. Then you allow trades between shares in A and B if and only if the trader can exhibit a proof of (A⟹B)∧(B⟹A). Hopefully the language has some reflection ability that allows you to determine which expressions are conjunctions or disjunctions or neither.
Related: https://lean-fro.org/about/ (automated theorem proving FRO)
I assume your proposal requires trades be public, so that someone exploiting a proof to get free money ends up revealing the proof to others.
Until computerized theorem proving vastly improves, this system will only prove statements after the first proof is accepted.
While I believe that this is a sensible proposal, I do not believe there will be too much of a market (in the near future) for it for societal reasons. Our current society unfortunately does not have a sufficient appreciation for mathematics and mathematical theorems for this to have much of a market cap. To see why this is the case, we can compare this proposal to the proposal for cryptocurrency mining algorithms that are designed to advance science. I propose that a scientific cryptocurrency mining algorithm should attract a much larger market capitalization than a theorem-proof market, but since scientific cryptocurrencies do not have much of a market, one should not expect for shares of theorems to attract much of a market either.
A market for mathematical conjectures requires participants to not only actively understand the mathematics behind the conjectures, but to also understand these theorems in their complete formalism. Perhaps AI systems may be developed to translate the formalism into English, but such a system may be flawed and may be subject to hacking in the sense that the statement in English may not be exactly the same as the formal statement, and it may be really easy to prove the formal statement. Since such a market requires a substantial amount of effort from the users, it is unlikely that there will be many users who are willing to put in the effort into understanding the mathematics along with the formalism.
It is also likely for the market to favor simple propositions that are easy to understand such as the bounded gaps between primes conjecture. For example, Beal’s conjecture states that there are no positive integers a,b,c,x,y,z with ax+by=cz and x,y,z≥3 and where a,b,c have no common factor. This conjecture was formulated by the billionaire Michael Beal. Beal attached a million dollar prize to this conjecture. This conjecture is a generalization of Fermat’s last theorem. Beal’s conjecture is a reasonably interesting conjecture, but it seems like Beal’s conjecture is the very best mathematics problem that amateur mathematicians can come up with and fund with one’s own money. This means that the market for mathematical theorems will be small and will mainly for theorems that anyone can understand such as the Twin Prime conjecture. It would be more satisfying if the market for mathematical theorems better represents the type of problems and questions that your typical mathematician were interested in.
Cryptocurrency mining algorithms can be used to solve scientific problems, but the users of the cryptocurrency do not even have to care very much about the underlying scientific problem. This is because a cryptocurrency is much more than its mining algorithm, and the details about the mining algorithm are relatively unimportant to the functionality of the cryptocurrency. If chosen correctly, the underlying scientific/mathematical problem does not harm or interfere very much with the cryptocurrency, so there is really no excuse for the cryptocurrency community to waste all those resources on cryptocurrencies on non-scientific problems because the cryptocurrency community does not have to. The cryptocurrency community needs to have a desire to not waste energy along with the philosophy that solving the most important scientific problem is profitable (this would be a self-fulfilling prophecy). The cryptocurrency community should also have a basic awareness of mining algorithms that are designed to solve a scientific problem (they do not need to know the specific details). This basic awareness should be part of the due diligence that every cryptocurrency enthusiast should partake in order to try to maximize profit, so this understanding should be natural for the cryptocurrency sector. Since there is still only one dominant minable cryptocurrency (namely Bitcoin), one only needs one scientific mining algorithm, so the cryptocurrency community does not even need to understand multiple scientific mining algorithms. They just need to know one. It is easier to know about one cryptocurrency mining algorithm than it is to know the market value of many theorems.
Right now Bitcoin has a market capitalization of about 500 billion dollars, and if Bitcoin was set up correctly, it could have had a mining algorithm that was designed to solve a very important scientific problem without the cryptocurrency community even thinking about this. Unfortunately, Bitcoin’s mining algorithm was never designed to advance science, and at this point, the cryptocurrency community is not very interested (due to anti-intellectualism) in using cryptocurrency technologies to solve any scientific problem. The cryptocurrency community to a great extent has no concept or understanding of Bitcoin or what it means for a cryptocurrency mining algorithm to solve a scientific problem. And those who think they understand what it means for a cryptocurrency mining algorithm to be designed to solve a scientific problem are quite antagonistic to cryptocurrency mining being used for any scientific purpose. Since the cryptocurrency community hates using cryptocurrency mining for a scientific purpose so much, one should expect for any market for proofs of theorems to be very small and undeveloped.
Nobody should expect for there to be a sizable theorem/proof market when that requires ~100 times as much effort from users than a market for cryptocurrencies with scientific mining algorithms and when there is no sizable scientific mining algorithm market.
With everything being said, we make a tradeoff with cryptocurrencies with scientific mining algorithms. Cryptocurrency mining algorithms such as SHA-256 must satisfy stringent conditions, so there are limited options in designing a cryptocurrency with a mining algorithm to advance science, and it is hard to fork a cryptocurrency to replace its scientific problem.
I would rather see people work on making scientific cryptocurrency mining more of a reality than imagining a market that is unlikely to exist any time soon because scientific cryptocurrencies are more feasible with the current state of the world.
With regards to subsidizing: all the subsidizer needs to do in order to incentivize work on P is sell shares of P. If they are short P when P is proven, they lose money—this money in effect goes to the people who worked to prove it.
To be more concrete:
Suppose P is trading at 0.50. I think I can prove P with one hour of work. Then an action available to me is to buy 100 shares of P, prove it, and then sell them back for $50 of profit.
But my going fee is $55/hour, so I don’t do it.
Then a grantmaker comes along and offers to sell some shares at $0.40. Now the price is right for me, so I buy and prove and make $60/hr.
As far as I can tell the subsidiser does not actually get a proof of the hypothesis. Is there a way in this system to pay to actually get the proof?