Bounties
Put a price on a proof
Pledge a reward for the first proof of a statement that qed.bot's checker admits: it builds at a pinned commit and rests on the standard axioms alone. The checker decides; the pledger pays. qed.bot holds no money.
Bounties
Loading bounties…
Pledge a bounty
How a bounty is settled
A claim is a link to a Lean file on GitHub. It is queued for the same checker that grades the register: the project is rebuilt at a pinned commit and every theorem's axioms are inspected. A claim is admitted only if the proof elaborates and rests on propext, Classical.choice and Quot.sound alone.
Whether the formal statement says what the bounty's statement says is a separate question, recorded on the problem's page as its fidelity grade. A pledger can add conditions, such as requiring a Comparator check against a named statement.
qed.bot records the pledge and the verdict. It does not hold, move or guarantee any payment; the reward is paid by the pledger directly.