Abstract
Solving open mathematical problems is hard to incentivize. Classical prize competitions pay a fixed amount to the first complete proof. They tie the reward neither to perceived difficulty nor to incremental progress, and they aggregate no information about which problems are considered solvable. Prediction markets aggregate exactly this kind of information in prices.
The central observation: formal verifiability of a proof gives a prediction market an objective settlement criterion. Ordinary event markets lack this, because their outcome depends on an oracle that must interpret the world.
On Proof Exchange, markets settle on proofs checked in Lean 4. Progress on the proof corresponds to an information advantage over the market. Thus even informal insights and partial contributions see attribution in the resulting price shift and corresponding payout.
Confirm by email, and we'll write when we open.