Prizes

Open prizes

Each prize is offered for a Lean 4 proof or disproof of one claim’s published formal statement, checked by a machine against Mathlib at a pinned revision and reviewed by the claim’s steward for whether the statement proved is the statement posted. Offering a prize does not change how a claim is assessed or how important the graph judges it to be; it says only that someone would like the question settled.

Prizes are stated and paid in owls, credit for metered work on the graph valued at one dollar of metered cost each and never redeemable for cash; a prize is taxable income at that value. The rules →

No prizes are open right now. A prize appears here when a mandate’s Grantmaker posts one, from that mandate’s own escrow, on a claim whose formal statement has passed its public review period.

Prizes are offered by Minerval, the sole obligor, in owls held against the escrow of the mandate that posted each one; no mandate promises the same owl to a prize and to an attempt. Every attempt by Minerval’s own solver on a prized statement is public with its cost and its report before the prize opens, so an outside claimant knows what has been tried.