Bounties
Pledge a reward for the first proof of a statement that qed.bot admits: it builds at a pinned commit, rests on the standard axioms alone, and proves the statement the register holds. Every bounty shows who pledged it, and appears only once its pledger confirms, with a code sent by email, that the address behind it works. qed.bot records the pledge and the checker's verdicts; the pledger pays the reward directly, and qed.bot holds no money.
Bounties
Loading bounties…
Pledge a bounty
How a bounty is published and settled
A bounty is published only after its pledger enters a six-digit code sent to the email address they give, which shows the address works. Until then nobody else can see it. The pledger's name and handle are shown with the bounty; the address is kept private.
A claim is a Lean file on GitHub, linked at its commit. First, the checker that grades the register rebuilds it and inspects every theorem's axioms: it passes only if the proof elaborates and rests on propext, Classical.choice and Quot.sound alone. Second, the proof must prove the statement the register holds: checked by the Lean kernel where the claim imports the register's formal statement, and otherwise confirmed by an administrator.
qed.bot records the pledge and the verdicts. It does not hold, move or guarantee any payment; the reward is paid by the pledger directly.