Revolutionizing Mathematics Funding
Imagining a market for mathematical proofs
tldr:
I put forward a possible Math Marketplace that would facilitate the buying and selling of mathematical proofs, powered by proof assistants. This would be valuable to industry, society, and the mathematicians themselves. This math marketplace would power an industry with unique properties, leading to interesting economic situations.
Present day:
A Network Company wants a solution to a graph theory puzzle; a solution would save them millions. That means it is time for some non-mathematicians at HR to choose a mathematician to hire or sponsor. They go with someone at a big university with fancy credentials.
Marvin is a math whiz who isn’t a fancy professor. There isn’t really a way for him to make money doing math, so society loses out on his genius as he takes a job doing something else. Maybe he does non-economically valuable math puzzles in his free time.
Grant approval processes are hellish.1
Mathematics funding can be much better
Math has a special advantage over most other fields: if it is right, it is easy to check that it is right. There are even computer programs called “proof assistants” that can verify that a proof is correct2! The way math is funded has not changed to make use of proof assistants.
Non-experts can know a proof is correct without understanding it or relying on a consensus of mathematicians.
How a Math Market might work
People with an interest in a mathematical question post a bounty.
Bid: $1,000,000 for an answer to: are there infinite twin primes?3 (Private, 5 years)
On the other side, mathematicians can sell proofs:
Ask: $900,000 for a proof that there are infinite twin primes.
The market above clears. Bids can be public or private. “Public” means that the proof will be added to a public repository anyone can view and use. “Private” means that the seller agrees to the proof becoming a trade secret of the buyer. The seller is under a legal agreement not to tell anyone else until a date set in the agreement.
Proofs rely on other proofs. A seller can write up most of a proof, leaving a few lemmas unproven. Then when proofs of those lemmas become available (either because the seller in turn posted bounties for them or the lemmas were posted publicly), the proof becomes complete and the seller gets paid. Math is complex, so math supply chains should be complex to keep up!
Roles
A new industry mean new ways to relate to the system: like in existing industries, there will be laborers, managers, and middlemen. Possibly criminals, too, but let’s work to avoid that.
Laborers:
The laborers in this system are the ones who complete a proof and claim a bounty.
Managers:
A manager would be someone who takes a problem and puts a private bounty on each chunk (and writes up a proof skeleton) such that all the chunks together form a complete proof of a problem with a bounty. Naturally, if a chunk is complicated there may be sub-managers.
Middlemen:
A middleman might spot that multiple proofs can be combined into one more general proof that would prove all the smaller cases or that a lemma is shared between many proofs. They might post a bounty for the shared proof at a value less than the sum that the middleman expects to claim. Sure, the laborer who solves the general proof could have collected all the bounties, but the middlemen are actually connecting the lemma to the proofs so I have fairly high confidence they are providing a real service.4
Automators:
There will be people making bots to write proofs to collect bounties. That’s not much of a problem; a proof is a proof. A math market could drive the development and evaluation of automated theorem proving programs.
Criminals:
Any time money is exchanging hands, there will be people trying to gain from the system without contributing anything. I would be irresponsible if I didn’t take a few minutes and foresee as many of the crimes people would attempt as possible.
Make a copy of a bounty, give it a lower price, and market it/draw attention to it.
That isn’t really a crime so much as a dishonest salesman. This is still not someone you would want on your platform.
“Hello stranger! Let’s work on this proof together. Send me your proof so far.”
Many proof assistants are real programming languages. To check proofs, our servers would kinda have to be running arbitrary user code. Not a generally safe thing to do, although luckily proofs need no IO. I think that means we just have to worry about denial of service attacks, but this is not something to take lightly.
Either the proofs stay on the user’s machines or they are sent to our servers. If they are sent to our servers, then we may have millions of dollars of proofs a hacker would want to steal. If they are only saved on user computers, then a valuable, profound, beautiful proof may be lost forever if the user drops their laptop in a pond or gets hit by a bus.
Possible uses for money laundering. (I don’t really know how money laundering works.)
If the math market is a for-profit organization that takes a cut of the money exchanged on the platform, it may be hard to stop users from simply contacting each other to exchange proofs. I think this is avoidable if we provide convenience and trust to our users (see the second criminal in this list). Online markets for games and other digital technology exists, so I expect one for proofs to work.
I’m concerned that criminals may post deceptively challenging problems to collect collaterals (see Finances)
Generally, I’m having trouble coming up with thefts and would love to hear your ideas in the comments! I feel like the system I’m describing is mostly just a pretty normal supply line, and you don’t hear about “thieves taking advantage of the chair industry,” but new frontiers mean new thefts until social systems, legal systems, and individuals can adjust.
Finances:
The platform would need ways to deal with some issues related to money.
Big proofs take a long time, and it would be a shame if the proof-buyer rescinded their offer right when a proof-seller was finishing up a year-long project or if a proof seller got scooped by someone else after spending a year working on it. Proof sellers need security which they should be able to buy by posting collateral. The collateral would “claim” the bid and “lock” the bid in place for an amount of time. If the proof-seller doesn’t solve the problem in time, the proof-buyer gets to keep the collateral and the bid is reopened to anyone else to solve. If the proof-seller solves it in time, they get their collateral back in addition to the bounty.
Money will be locked up in the platform for long periods of time. It would lose our users large amounts of money not to avoid inflation by placing bids and collaterals in liquid securities like stocks while they wait for someone to win them.
I spent a moment considering whether cryptocurrency would help. Considering that the goal is to get the system to be widely adopted and trusted and cryptocurrency is justly associated with speculators and fraudsters, including cryptocurrency in this plan would be counterproductive.
Loan system: Mathematicians need to eat while they are working on math. Currently, full-time mathematicians — PhD students and professors — go through a competitive, costly, and unpleasant grant application process to get stable income. The Math Market platform would have a comparative advantage over traditional banks in issuing loans since we would be able to collect data on an applicant’s ability to claim bounties. The loans the Market issues could effectively transfer money from the mathematician’s future to the past and smooth out the irregular income that comes from a career of occasionally claiming a large bounty.
Similarly: insurance. Mathematicians are taking risks when they attempt big projects. Failure-to-Solve insurance could protect the mathematicians from this risk.
A patent-like system without first-mover advantage: Jeff Bezos founded Amazon. Because he was the first big online retailer, he is now the second richest person in the world. Someone else would have done it if he hadn’t, so the value Bezos provided society was in giving the world online retailing a few years (or possibly months) earlier than otherwise. That is certainly a valuable service to provide society, worthy of vast amounts of money, but because his company controls the sector, he keeps getting richer far beyond the value he provided to society. The Math Market could offer a system where people could charge fees for others to use their proofs. The first person to make a proof would have control over the market exactly until the next person managed to remake that proof, so the innovator would capture exactly the value that they generate.
It isn’t ideal for two people with code for the same proof to drop their prices to zero due to infinite-supply perfect-competition because then the second person makes no money despite providing value to buyers by breaking the monopoly. I’m not seeing how the sellers can jointly negotiate with buyers.
If a public proof is posted, then the proof becomes free and none of the provers make money off of it anymore.
An interesting issue is that offering to sell someone a proof of x tells the prospective buyer that a proof of x exists. That may make such a patent system impossible! Other products don’t work this way; knowing that a mousetrap exists doesn’t mean that you no longer need to buy the mousetrap if you want to use it!
Problems:
Why doesn’t something like this already exist?
Would there be sufficient buyers for the system to work?
Would this mesh well with mathematicians looking for prestige?
Mathematicians losing internal motivation when they start to be provided with money for their projects is a legitimate worry.
On priors I expect ‘getting paid’ to be an improvement to the situation of humanity’s mathematicians because usually society gets more of what it pays for.
Hopeful future:
A Network Company wants a solution to a graph theory puzzle; a solution would save them millions. An employee who understands the problem but is not a mathematician — like a physicist or a programmer — will write the goal they want proven in a proof assistant language and will post a bounty on the Math Market.
Marvin is a math whiz who isn’t a fancy professor. In his free time he will browse the Math Market for problems he can solve, making good part-time money.
The project to formalize Fermat’s Last Theorem will have a bounty. Managers will break the problem into chunks that mathematicians can make money by solving.
Most mathematicians will no longer need to rely on grants for funding, and more mathematicians are able to make math their career.
Average proposal takes the Principal Investigator 116 hours and Chief Investigator 55 hours. And grants are often rejected. Ouch.
The Natural Number Game is a legitimately really fun game for learning the proof assistant language “Lean.” Even if you aren’t good at math or coding, I encourage you to try out the first few levels. Since it is a well-designed game, it starts easy and ramps up! It kept me obsessed and in the zone for days.
Similarly, grocery stores are providing a real service even though farmers technically could just sell the food to consumers directly.