Speculations on Adoption of Theorem Marketplaces
A response to theorem-marketplace.com
This post is a response to Vadim at the Rat and Tiger Substack. Vadim has recently brought to reality an exciting concept: A website where you can post and collect bounties on formal proofs of mathematical theorems1. This work brings together my interests in formal methods and blockchain technology, so I am really the ideal audience for it. In his post, Vadim raises what he calls the "community problem", and I would like to offer some thoughts on that.
The Currency of Academia as Reputation
Vadim comments:
People do pay for mathematics, after all; they do it all the time; mathematicians get their salaries from somewhere.
This is indeed a fruitful thought in this context, and it's worth considering who it is that pays the salaries of mathematicians. You could also ask who pays the salary of the type of person who knows how to write formal proofs of theorems. In either case, given the level of technical expertise involved, the sort of person we are talking about seems likely to be some sort of academic.
Who pays the salary of academics? Universities do, but more indirectly, their revenue stream comes from government grants, student tuition, and alumni donations. To induce these funding sources to pay for research, it's important that the mathematicians working at the university have a reputation for proving interesting and important theorems. Whether theorems are interesting and important is judged by experts, who are themselves other mathematicians working at other universities, so in an even more indirect way, you could say academics decide on other academics’ salaries in a sort of recursive loop.
This is all to say that academia is a bit of a weird environment where success is based heavily based on reputation, unlike, say, the business world, where success is based on profitability.
I think this poses challenges for the adoption of theorem marketplaces:
The people who are most capable of writing formal proofs of theorems are fairly few.
Those people likely already have a job at a university (or maybe they have left academia, but still are probably employed).
The fact that someone is offering to pay for a particular theorem is a sign that they don't have the reputation to get it done for free2. Thus, neither posting the problem nor solving the problem are particularly likely to be reputation-improving, and so won’t be of direct interest.
Perhaps the involvement of money is itself somehow seen as venal, particularly if the money is cryptocurrency3.
Government Funding Agencies will probably not want to fund bounties, since there are the PR risks that the bounty will never be claimed, or be claimed by some persona non grata, or, heaven forbid, be claimed by a foreigner.
So who will prove the theorems?
The dissonance between the academic mindset and the economics of the theorem marketplace is a headwind. But, just as many problems in mathematics can be solved with a change in perspective, I think there are some avenues that might make a version of the theorem marketplace idea more viable:
AIs
One way of getting around the problem of not having anyone to prove theorems is to just build a machine to do it. A nice benefit of this approach is that once you have one AI, you can set it loose on the entire database of theorems that have been posted to the marketplace. A few good AIs could provide most or all of the supply-side of the market. The drawback is that the technology may not be ready. Is it?
There have been some exciting recent advancements in the capabilities of AI theorem provers. Most notably, and most relevant to the Lean-based theorem marketplace that Vadim has created, is DeepMind's AlphaProof, which was able to formally prove a number of statements from the most recent International Mathematical Olympiad. Unless the program got lucky, this is a very impressive result. Certainly the IMO theorems it has successfully proven feel more difficult than lemmas I have been frustrated by in my own formalization work - If I ask myself whether I would have been willing to pay for a proof of one of those lemmas, the answer is yes. On the other hand, if I ask myself whether I would have been willing to pay an amount commensurate with the cost of the GPU time that AlphaProof may have used on the IMO4, my answer is more doubtful.
There are a lot of unknowns here:
How much does it really cost to run AlphaProof?
How does that cost (and demand) scale with the difficulty of the problem in question?
When will something like AlphaProof be generally available?
How easy will it be for other labs to improve upon what has been done, both in terms of cost and capability?
Whatever the answers to these questions, it seems like the AI approach will require time to mature, which means that the theorem marketplace will have to be patient if it wants to leverage this technology.
Change the currency to one that is more acceptable to academics
Another avenue to getting more adoption might be to change the bounties from money to something more reputational. One way to do this, simple as it sounds, would be to make sure that the claimant of a bounty has their username prominently displayed on the bounty webpage. Certainly it seems to be the case that the Lean mathlib library is careful to credit its contributors: It does so in authorship lines of files, in Github pull request headers, and on the tracking pages for important theorems.
Another idea, more cryptocurrency-related, could be something along the lines of "hypercerts". This is an interesting idea that I followed for a while a few years ago: It looks to issue certificates for various forms of public good provision, with the idea that these certificates can perhaps be traded. Central to the philosophy of hypercerts is that the certificates are a way of assigning credit. The theorem marketplace has the benefit that it is easy to verify that a proof has been done, so there can be no debate over whether a hypercert should be awarded. The downside is that the idea is very associated with blockchain technology, so there will be a negative association for some.
Who will provide the bounties?
We still have to talk about the demand side of the theorem marketplace. Who will be willing to pay for theorems to be proven? Here are some possibilities:
The Erdőses of the World
As a counterpoint to my claim that mathematics is an academic field which is contrary to the idea of paying for proofs, I'll point out that there does seem to be a subculture within math that likes the idea of monetary prizes. This subculture is maybe more associated with the second of the "Two Cultures of Mathematics" that W. T. Gowers talks about in his essay so titled. The archetype of this subculture is Paul Erdős, who famously offered cash prizes for solutions to problems he was interested in.
Does this type of mathematician exist today? Perhaps. There are certainly mathematicians who will put bounties on problems they are interested in on MathOverflow, but these bounties are for internet points, and therefore more reputational than monetary. I certainly have a backlog of problems I've considered before, and I would probably be willing to put bounties on them5. But there are limits to how much I would be willing to spend, and I doubt the inflow of money from people like me would be able to sustain many or any career freelance theorem bounty hunters. So this seems like a possibility, but not one that is going to make the theorem marketplace the go-to hub for buying and selling proofs.
The Clay Institutes of the World
The Millenium Prize Problems are a more serious example of this type of thing - at least in terms of the magnitude of money. The Clay Mathematics Institute has put up a million dollars for the solution to each of seven problems. The existence of prizes like this bodes well for the theorem marketplace, but it's a bit discouraging that the only problems that can command this kind of bounty seem to be so fiendishly difficult - The prizes have been up for 24 years, and only one has been solved6. I unfortunately don't have any advice to offer about how to get an institution like this to decide to put up their bounties in formally verifiable form.
The Crypto-Millionaires of the World
Since the theorem marketplace we are talking about is designed around a blockchain, it makes sense to consider cryptocurrency users as a potential source of bounties. The Ethereum Foundation has even started to fund formal verification of cryptography, which seems like a great synthesis of the needs of the crypto community with the use of formal methods. Perhaps in the future, this sort of funding can have an on-the-blockchain form.
There is an intriguing thesis that the main benefit of cryptocurrency is not the technology itself, but that it has made rich people who now see themselves as torchbearers for financial technology as a force for progress. Could these people be convinced to put up bounties for theorems? My suspicion is that this is a possibility, but that there would have to be some kind of angle. One could imagine crypto entrepreneurs taking a version of the theorem prover marketplace that Vadim has created and making an even more crypto-y version of it (e.g. "One percent of all bounties will be tokenized and used to fund development of the platform"). Whether such a proposal would succeed is hard to say, since the more complicated and extractive the system seems, the more it will turn off some potential users.
Conclusion: Is this idea doomed?
The proposals here leave a somewhat mixed view of the potential for the theorem marketplace idea. The idea has the potential to be the future of how mathematics is done, but the problem with futuristic ideas is that they often remain in the future. I don't think this means that this kind of thing absolutely shouldn't be worked on - new technology has to come about somehow and every tech startup has a chance of failure. But I think it's important to be realistic about how hard community building can be. Whatever the future of the theorem marketplace, I think what already exists is very cool, and I am interested to see where it goes.
In the interest of a quantifiable prediction, I put up this prediction market on the number of monthly users of this kind of technology in two years. My forecast is:
Theorem marketplaces are abandoned as an idea - they don't exist / no one regularly uses them. ~20%
Theorem marketplaces are extremely niche - 1-6 people regularly use them. ~60%
Theorem marketplaces have a small community - 7-48 people regularly use them. ~12%
Theorem marketplaces have a healthy community - 49-342 people regularly use them ~5%
Theorem marketplaces are a broadly helpful tool - 343-2400 people regularly use them ~2%
Theorem marketplaces are a thriving ecosystem - 2401+ people regularly use them ~1%
Note - the website currently uses the Sepolia Ethereum testnet, so no real money is yet at stake. Nevertheless, it's a good proof of concept.
Converse case in point - See how much great work has been put into the Equational Theories Project. Seems like a key factor in getting the ball rolling with this project was Terence Tao's reputation.
See this comment from the Lean forum thread where the theorem marketplace was announced. The difference between the way blockchain proponents think about "trust" vs. others is an interesting topic, I might recommend Ezra Klein's interview of Vitalik Buterin for more on this, but unfortunately it's paywalled.
AlphaProof took 3 days for at least some of the problems it solved. Googling tells me 3 days of GPU time costs $72-$400, but we don't know how many GPUs AlphaProof was using.
Although in that case, the solver declined the prize, saying that another mathematician had done more work on the problem (ref). Why he didn't simply accept the prize and give away the money, I don't know - I think the anecdote supports my claim about the troubled relationship between academics and money. I think there is an important lesson here for theorem proving bounties about the importance of rewarding not just the finishers of problems, but also contributors of libraries and "theory builders". How best to do this is something I've discussed a little on Zulip, but I think it's a fascinating and challenging "cryptoeconomic" problem, perhaps best left to another post.