The Proof Bounty

Formalizing mathematics requires choosing what to prove next. In a centralized system, a planner surveys the landscape and assigns tasks. This works until the landscape is too large or too unfamiliar for any single planner to survey effectively — which is the usual case in serious formalization efforts.

Brown, Kaliszyk, and Urban replace planning with pricing. Multiple LLM agents operate in a simulated bounty marketplace where they can propose lemmas, attach bounties to unsolved ones, and compete to prove them. An agent that needs a lemma but can’t prove it posts a bounty. An agent that can prove it claims the reward. The proof assistant verifies everything — no agent trusts another agent’s work.

The agents don’t just prove assigned theorems; they introduce definitions and intermediate lemmas to organize the mathematical development. The structure of the formalization emerges from the market rather than from a plan. What gets formalized first is what’s most needed — the lemmas with the highest bounties, which are the ones blocking the most other proofs.

The through-claim: coordination through prices can replace coordination through planning when the task space is too large for any single agent to survey. The bounty doesn’t encode understanding of the mathematical landscape — it encodes demand. An agent posting a high bounty on a lemma doesn’t need to know why that lemma matters globally; it just needs to know that it’s stuck without it. The price signal aggregates local needs into global priorities without anyone computing the global picture. Mathematics formalization becomes a market problem, and markets solve coordination problems that planners cannot.