Legal
Terms of service
Draft. This page exists because we take payments from users in the EU and the obligation is not optional. The wording below is a placeholder and has not been reviewed by a lawyer.
What you are buying
A credit buys one verification attempt. It does not buy a reward, and it does not guarantee that a submitted proof will be accepted.
Refunds
A credit is refunded when the failure is ours — a configuration error or an infrastructure outage. What happens to a credit when the kernel rejects a proof, and what happens to work invalidated by a pin rotation, is not yet settled. We would rather leave that open here than state a policy we have not agreed.
Rewards
Bounties are advertised in USD and paid in alpha; no fixed conversion rule is published, and the figure shown on a problem page carries the rate and the time it was taken. The advertised pool deliberately exceeds the treasury balance, and both figures are shown publicly. How a duplicate solve is treated — if two people prove the same statement — is not yet settled either.
Disqualification
Submitting a proof copied from an unmerged pull request or from a public source, or exploiting the Lean kernel rather than proving the statement, disqualifies that submission from reward.