Welcome to The Nonlinear Library, where we use Text-to-Speech software to convert the best writing from the Rationalist and EA communities into audio. This is: Logical Share Splitting, published by DaemonicSigil on September 11, 2023 on LessWrong.

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 A⟺B then a share in A can be exchanged for a share in B. 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 A⟹B, then we show A. This allows us to prove B. 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 B, even if one trader can only prove A⟹B and the other trader can only prove A. So let's say there's some profit in pro...